| ae77c0b | Dominique Larchey-Wendling | 07 May 2021, 10:19:59 UTC | typo in summary.v reduction --> ireduction | 07 May 2021, 10:19:59 UTC |
| 92096e9 | Dominique Larchey-Wendling | 01 May 2021, 08:04:38 UTC | Merge branch 'coq-8.13' into try_merge | 01 May 2021, 08:04:38 UTC |
| 51bad07 | Dominique Larchey-Wendling | 01 May 2021, 08:02:03 UTC | italic | 01 May 2021, 08:02:03 UTC |
| 32c63a6 | Dominique Larchey-Wendling | 01 May 2021, 07:57:04 UTC | link to "Manual instructions" | 01 May 2021, 07:57:04 UTC |
| 2d6f7e7 | Dominik Kirst | 30 April 2021, 15:29:29 UTC | epsilon | 30 April 2021, 15:29:29 UTC |
| 700c1ed | Dominik Kirst | 30 April 2021, 15:26:30 UTC | installation instructions | 30 April 2021, 15:26:30 UTC |
| 84570da | Dominique Larchey-Wendling | 29 April 2021, 14:41:52 UTC | added informations for Lemmas 54 & 55 | 29 April 2021, 14:41:52 UTC |
| 23df568 | Dominique Larchey-Wendling | 29 April 2021, 13:28:37 UTC | Merge branch 'improv_trak_8.13' of github.com:DmxLarchey/coq-library-undecidability into improv_trak_8.13 | 29 April 2021, 13:28:37 UTC |
| a5400a7 | Dominique Larchey-Wendling | 29 April 2021, 13:26:25 UTC | added sep_logic to summary.v | 29 April 2021, 13:26:25 UTC |
| c3d5652 | Dominik Kirst | 29 April 2021, 13:12:19 UTC | coqdoc fix | 29 April 2021, 13:12:19 UTC |
| 4ed21e7 | Dominik Kirst | 29 April 2021, 11:39:06 UTC | added seplog links in summary file | 29 April 2021, 11:39:06 UTC |
| 3b41b89 | Dominique Larchey-Wendling | 29 April 2021, 11:00:14 UTC | Put all "Print Assumptions" in comments to avoid bugging the CI which takes too long with them | 29 April 2021, 11:00:14 UTC |
| 07ed00c | Dominique Larchey-Wendling | 29 April 2021, 10:15:24 UTC | uploaded and UPDATED the summary.v file, with the correct numbering of Lemmas/Facts/Thms/Defs and the addition of the new results. | 29 April 2021, 10:15:24 UTC |
| 97628fc | Dominique Larchey-Wendling | 26 April 2021, 22:27:19 UTC | change the notation for discerning functions to greek letters to agree with the paper | 26 April 2021, 22:27:19 UTC |
| c6d1e81 | Dominique Larchey-Wendling | 23 April 2021, 16:32:52 UTC | Merge pull request #126 from DmxLarchey/imsell-8.13 Improvements (notations, shorter proofs, etc) for IMSELL | 23 April 2021, 16:32:52 UTC |
| 87c8e77 | Dominique Larchey-Wendling | 23 April 2021, 14:13:31 UTC | Merge branch 'coq-8.13' into imsell-8.13 | 23 April 2021, 14:13:31 UTC |
| 8e50d80 | Dominique Larchey-Wendling | 23 April 2021, 14:01:30 UTC | forgot to commit that correction | 23 April 2021, 14:01:30 UTC |
| 95f9062 | Yannick Forster | 23 April 2021, 13:17:47 UTC | Merge pull request #125 from yforster/coq-8.13-update-README Update README in 8.13 branch | 23 April 2021, 13:17:47 UTC |
| d59f976 | Dominique Larchey-Wendling | 23 April 2021, 12:20:57 UTC | Merge branch 'coq-8.13' into imsell-8.13 | 23 April 2021, 12:20:57 UTC |
| e4d2b50 | Yannick Forster | 23 April 2021, 08:47:57 UTC | Update README | 23 April 2021, 08:47:57 UTC |
| 6094fb8 | Dominique Larchey-Wendling | 22 April 2021, 18:17:07 UTC | New version of TRAKHTENBROT merged with coq-8.13 | 22 April 2021, 18:17:07 UTC |
| 1da3a10 | Dominique Larchey-Wendling | 22 April 2021, 16:38:42 UTC | Merge branch 'coq-8.13' into improv_trak_8.13 | 22 April 2021, 16:38:42 UTC |
| f88f319 | Dominique Larchey-Wendling | 21 April 2021, 09:36:50 UTC | Merge branch 'coq-8.12' into imsell | 21 April 2021, 09:36:50 UTC |
| f4ff9aa | Dominique Larchey-Wendling | 20 April 2021, 00:07:21 UTC | names w/o \Sigma symbol because of http links | 20 April 2021, 00:07:21 UTC |
| 5b15a2f | Dominique Larchey-Wendling | 19 April 2021, 16:25:41 UTC | displaced a notation def on top of the file | 19 April 2021, 16:25:41 UTC |
| acf343f | Dominique Larchey-Wendling | 19 April 2021, 16:13:45 UTC | restructured the files, added Sig_discernable.v and moved high-level results in red_dec.v | 19 April 2021, 16:13:45 UTC |
| 21f7598 | Dominique Larchey-Wendling | 17 April 2021, 23:42:30 UTC | change of two names | 17 April 2021, 23:42:30 UTC |
| 2b10aaa | Dominique Larchey-Wendling | 15 April 2021, 14:34:18 UTC | cosmetic | 15 April 2021, 14:34:18 UTC |
| 56c4a0d | Dominique Larchey-Wendling | 15 April 2021, 14:23:23 UTC | finished the characterisation of decidability of FSAT by decidability of discernability of function and relation symbols | 15 April 2021, 14:23:23 UTC |
| 01f01f7 | Dominique Larchey-Wendling | 15 April 2021, 09:00:08 UTC | some cleanup in names and intermediate statements | 15 April 2021, 09:00:08 UTC |
| 53531d4 | Dominique Larchey-Wendling | 15 April 2021, 08:14:18 UTC | proof that FSAT is decidable if either a) syms and rels have decidable discernability and all arities are <= 1 b) rels have decidable discernability and rels arity are all 0 | 15 April 2021, 08:14:18 UTC |
| e4f900f | Dominique Larchey-Wendling | 14 April 2021, 20:46:16 UTC | nearly finished proof that signatures of uniform arity 1 have decidable FSAT iff both funs and rels have decidable discernability | 14 April 2021, 20:46:16 UTC |
| 306ad57 | Dominique Larchey-Wendling | 14 April 2021, 10:47:43 UTC | proof that FSAT decidability is equivalent to decidable discernability for purely monadic signatures (ie. function function symbols), finiteness assumption is removed | 14 April 2021, 10:47:43 UTC |
| b5f6b87 | Yannick Forster | 14 April 2021, 08:23:09 UTC | Merge pull request #121 from uds-psl/yforster-patch-1 Add mu recursive functions to README | 14 April 2021, 08:23:09 UTC |
| 38d97c5 | Yannick Forster | 12 April 2021, 09:21:53 UTC | Add mu recursive functions to README | 12 April 2021, 09:21:53 UTC |
| 26a8473 | Dominique Larchey-Wendling | 11 April 2021, 22:41:53 UTC | better characterization of FSAT on a finite pure monadic signature with X as type of relations, FSAT is decidable iff X is discriminable where discriminable means there is a discerning map to a discrete type | 11 April 2021, 22:41:53 UTC |
| 9d8b483 | Dominique Larchey-Wendling | 06 April 2021, 23:58:03 UTC | a better tactic notation for proving equivalences by structural analysis | 06 April 2021, 23:58:03 UTC |
| 0d79d38 | Dominique Larchey-Wendling | 06 April 2021, 22:39:29 UTC | better notations, mostly | 06 April 2021, 22:39:29 UTC |
| 6efbd21 | Dominique Larchey-Wendling | 01 April 2021, 23:04:51 UTC | reordered membership to avoid meta-level hypothesis of finiteness and dec to polute FOL results | 01 April 2021, 23:04:51 UTC |
| 2ac08fc | Dominique Larchey-Wendling | 01 April 2021, 22:46:35 UTC | removed most Let from reln_hfs.v plus simplified a bit | 01 April 2021, 22:46:35 UTC |
| c9c39f2 | Dominique Larchey-Wendling | 01 April 2021, 11:52:26 UTC | further simplified reln_hfs and Sign -> Sig2 reduction | 01 April 2021, 11:52:26 UTC |
| aa4845e | Dominique Larchey-Wendling | 30 March 2021, 00:04:25 UTC | small change in wf_finite_t, simplification | 30 March 2021, 00:04:25 UTC |
| 0f7d442 | Dominique Larchey-Wendling | 29 March 2021, 22:24:00 UTC | better notations on wf_finite | 29 March 2021, 22:24:00 UTC |
| 927df37 | Dominique Larchey-Wendling | 29 March 2021, 16:44:26 UTC | Local Notations | 29 March 2021, 16:44:26 UTC |
| 49022a7 | Dominique Larchey-Wendling | 29 March 2021, 16:42:25 UTC | cleanup in discrete.v, better notations, length in the weak powerset | 29 March 2021, 16:42:25 UTC |
| 54550f6 | Yannick Forster | 29 March 2021, 11:53:46 UTC | Merge pull request #116 from dominik-kirst/seplogic Separation Logic | 29 March 2021, 11:53:46 UTC |
| 0f3fd61 | Dominik Kirst | 19 March 2021, 12:48:02 UTC | improved readme and changed file and problem names | 19 March 2021, 12:48:02 UTC |
| 1ed38fe | Dominik Kirst | 19 March 2021, 12:25:52 UTC | quantifier notations in comments | 19 March 2021, 12:25:52 UTC |
| bde7a60 | Dominik Kirst | 19 March 2021, 12:21:23 UTC | Merge pull request #1 from DmxLarchey/seplogic-dlw A module for FOL notations within TRAHKTENBROT | 19 March 2021, 12:21:23 UTC |
| 9db05e0 | Dominique Larchey-Wendling | 19 March 2021, 12:01:41 UTC | A module for fol_notations | 19 March 2021, 12:01:41 UTC |
| 91bd889 | Dominik Kirst | 18 March 2021, 16:30:16 UTC | proof using flag | 18 March 2021, 16:30:16 UTC |
| 6bf9427 | Dominik Kirst | 18 March 2021, 16:16:43 UTC | readme | 18 March 2021, 16:16:43 UTC |
| 9d81434 | Dominik Kirst | 18 March 2021, 14:23:56 UTC | cleanup | 18 March 2021, 14:23:56 UTC |
| 09388f0 | Dominik Kirst | 17 March 2021, 17:17:28 UTC | undec files | 17 March 2021, 17:17:28 UTC |
| b5d9983 | Dominik Kirst | 17 March 2021, 11:34:48 UTC | reduction from trakhtenbrot to new fsat | 17 March 2021, 11:34:48 UTC |
| a000c6c | Dominik Kirst | 17 March 2021, 10:30:00 UTC | switched quantifier notation | 17 March 2021, 10:30:00 UTC |
| 41bf7a2 | Dominik Kirst | 16 March 2021, 17:26:24 UTC | reduction for closed FSAT | 16 March 2021, 17:26:24 UTC |
| 0bb50d8 | Dominik Kirst | 15 March 2021, 13:21:49 UTC | finished rest of requirements | 15 March 2021, 13:21:49 UTC |
| e23c755 | Dominik Kirst | 15 March 2021, 12:45:13 UTC | half of missing requirements | 15 March 2021, 12:45:13 UTC |
| 0a2e328 | Dominik Kirst | 12 March 2021, 17:27:48 UTC | done up to model requirements | 12 March 2021, 17:27:48 UTC |
| b32e2a1 | Dominik Kirst | 12 March 2021, 16:39:31 UTC | finished up to requirements and final proof | 12 March 2021, 16:39:31 UTC |
| a5b5683 | Dominik Kirst | 12 March 2021, 16:17:57 UTC | closed main proofs | 12 March 2021, 16:17:57 UTC |
| bb831c2 | Dominik Kirst | 12 March 2021, 14:21:38 UTC | improvements | 12 March 2021, 14:21:38 UTC |
| 24712de | Dominik Kirst | 12 March 2021, 11:38:53 UTC | backwards direction | 12 March 2021, 11:38:53 UTC |
| 6dd38f5 | Dominik Kirst | 11 March 2021, 17:34:08 UTC | encoding function from FOL FSAT to min_seplogic | 11 March 2021, 17:34:08 UTC |
| 46d0fb2 | Dominik Kirst | 11 March 2021, 12:17:00 UTC | switched to de bruijn syntax | 11 March 2021, 12:17:00 UTC |
| 705dd73 | Dominik Kirst | 10 March 2021, 18:29:44 UTC | functionality constraint | 10 March 2021, 18:29:44 UTC |
| 368e469 | Dominik Kirst | 10 March 2021, 16:17:04 UTC | epsilon | 10 March 2021, 16:17:04 UTC |
| b796dc9 | Dominik Kirst | 10 March 2021, 16:15:57 UTC | example and little fix | 10 March 2021, 16:15:57 UTC |
| fad7b10 | Dominik Kirst | 10 March 2021, 15:19:55 UTC | two fragments of separation logic | 10 March 2021, 15:19:55 UTC |
| 77276a0 | Yannick Forster | 10 March 2021, 09:29:45 UTC | Merge pull request #113 from yforster/neq_coq-8.13 Merge 8.12 into 8.13 to prepare for opam release | 10 March 2021, 09:29:45 UTC |
| a9d60ea | Yannick Forster | 02 March 2021, 14:23:54 UTC | Use MetaCoq 1.0~beta2 on coq-8.12 (#114) * use MetaCoq 1.0~beta2, getting rid of the checker dependency * fix Extract.v * fix GenEncode.v * remove broken and unused Notation * fix rewrites | 02 March 2021, 14:23:54 UTC |
| cfcd4c7 | Yannick Forster | 02 March 2021, 14:22:59 UTC | Merge pull request #1 from mrhaandi/neq_coq-8.13 fixed warnings | 02 March 2021, 14:22:59 UTC |
| 4690ec2 | Andrej Dudenhefner | 02 March 2021, 13:01:02 UTC | fixed warnings set coq to 8.13.1 | 02 March 2021, 13:01:02 UTC |
| 100c9a1 | Dominique Larchey-Wendling | 26 February 2021, 14:02:51 UTC | divides_dec in fractran_step_dec | 26 February 2021, 14:02:51 UTC |
| 30e0c1a | Yannick Forster | 24 February 2021, 08:40:39 UTC | fix setoid rewriting bug | 24 February 2021, 08:40:39 UTC |
| 5a651b9 | Dominique Larchey-Wendling | 23 February 2021, 22:38:25 UTC | change the reduction chain FRACTRAN <= MMA2 <= MM2 <= ndMM2 to FRACTRAN <= MMA2 <= ndMM2 | 23 February 2021, 22:38:25 UTC |
| 7883c17 | Yannick Forster | 23 February 2021, 09:58:04 UTC | fix FOL under 8.13 | 23 February 2021, 09:58:04 UTC |
| fb04c32 | Yannick Forster | 23 February 2021, 09:01:12 UTC | fix typo in MetaCoq version | 23 February 2021, 09:01:12 UTC |
| 1f3e551 | Yannick Forster | 23 February 2021, 08:00:16 UTC | restart CI | 23 February 2021, 08:00:16 UTC |
| 97d5db4 | Dominique Larchey-Wendling | 22 February 2021, 22:55:21 UTC | more generic def of MMA_PROBLEM | 22 February 2021, 22:55:21 UTC |
| 6347f0d | Yannick Forster | 22 February 2021, 16:15:44 UTC | fix equations version | 22 February 2021, 16:15:44 UTC |
| fb0c262 | Yannick Forster | 22 February 2021, 16:00:57 UTC | use released MetaCoq packages | 22 February 2021, 16:00:57 UTC |
| b6d68dd | Yannick Forster | 22 February 2021, 15:56:54 UTC | Merge branch 'coq-8.12' into neq_coq-8.13 | 22 February 2021, 15:56:54 UTC |
| 8e170e6 | Dominique Larchey-Wendling | 22 February 2021, 08:53:32 UTC | slight ups | 22 February 2021, 08:53:32 UTC |
| 8afdc22 | Dominique Larchey-Wendling | 15 February 2021, 14:51:53 UTC | small ups in notations mostly | 15 February 2021, 14:51:53 UTC |
| 9396e87 | Dominique Larchey-Wendling | 08 February 2021, 15:04:46 UTC | loops no needed anymore | 08 February 2021, 15:04:46 UTC |
| 19822b1 | Dominique Larchey-Wendling | 06 February 2021, 23:28:08 UTC | forgot to update some code for the small changes | 06 February 2021, 23:28:08 UTC |
| 97e9e19 | Dominique Larchey-Wendling | 06 February 2021, 23:18:57 UTC | removed the need of super-regularity ... the reduction already worked for regular Fractran programs | 06 February 2021, 23:18:57 UTC |
| 6830557 | Dominique Larchey-Wendling | 06 February 2021, 23:00:31 UTC | Notations mostly | 06 February 2021, 23:00:31 UTC |
| c6b3cd0 | Dominique Larchey-Wendling | 02 February 2021, 23:45:41 UTC | change in notation for shorter notations | 02 February 2021, 23:45:41 UTC |
| 8b870ad | Dominique Larchey-Wendling | 02 February 2021, 13:52:22 UTC | Merge remote-tracking branch 'upstream/coq-8.12' into mma_ndmm | 02 February 2021, 13:52:22 UTC |
| 24aec42 | Dominique Larchey-Wendling | 02 February 2021, 13:39:29 UTC | changed "by lia" into "unfold z2; lia" in SMN_transform.v Do not know why "by lia" failed in Coq 8.12.0 ? | 02 February 2021, 13:39:29 UTC |
| 37f3507 | Dominique Larchey-Wendling | 02 February 2021, 13:20:38 UTC | a shared reduction from FRACTRAN_REG_HALING to both MMA2_HALTING and MMA2_HALTS_ON_ZERO. This avoids the detour through the compiler for the reduction from MMA2_HALTING to MMA2_HALTS_ON_ZERO, hence avoids having to describe it in a paper | 02 February 2021, 13:20:38 UTC |
| bcdf0e8 | Yannick Forster | 30 January 2021, 12:53:43 UTC | Merge pull request #111 from dominik-kirst/itp Peano Arithmetic, Binary ZF, Binary FOL | 30 January 2021, 12:53:43 UTC |
| c7c88f4 | Dominik Kirst | 30 January 2021, 11:44:29 UTC | readme, using vector notations, moved syntax fragments | 30 January 2021, 11:44:29 UTC |
| 17193a5 | Dominik Kirst | 29 January 2021, 21:56:48 UTC | incompleteness proof up to enumerability | 29 January 2021, 21:56:48 UTC |
| eb1d468 | Marc Hermes | 29 January 2021, 20:24:40 UTC | changes in Axiomatisations | 29 January 2021, 20:24:40 UTC |
| 53795e0 | Dominik Kirst | 27 January 2021, 18:02:21 UTC | refactored H10p reduction | 27 January 2021, 18:02:21 UTC |
| 4c08471 | Marc Hermes | 26 January 2021, 16:51:23 UTC | Merge branch 'itp' of https://github.com/dominik-kirst/coq-library-undecidability into itp | 26 January 2021, 16:51:23 UTC |
