| 6760922 | Dominique Larchey-Wendling | 23 April 2021, 16:34:27 UTC | Merge pull request #122 from DmxLarchey/imsell Improvements (notations, shorter proofs, etc) for IMSELL | 23 April 2021, 16:34:27 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 |
| 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 |
| 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 |
| 100c9a1 | Dominique Larchey-Wendling | 26 February 2021, 14:02:51 UTC | divides_dec in fractran_step_dec | 26 February 2021, 14:02:51 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 |
| 97d5db4 | Dominique Larchey-Wendling | 22 February 2021, 22:55:21 UTC | more generic def of MMA_PROBLEM | 22 February 2021, 22:55:21 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 |
| b197e1b | Marc Hermes | 26 January 2021, 16:51:15 UTC | added Axiomatisations.v | 26 January 2021, 16:51:15 UTC |
| 0ed4b81 | Dominik Kirst | 26 January 2021, 12:42:39 UTC | reductions without assumptions | 26 January 2021, 12:42:39 UTC |
| c4b8861 | Dominik Kirst | 26 January 2021, 11:19:00 UTC | undec of binary FOL | 26 January 2021, 11:19:00 UTC |
| e3eafec | Dominik Kirst | 26 January 2021, 10:26:13 UTC | Merge branch 'itp' of https://github.com/dominik-kirst/coq-library-undecidability into itp | 26 January 2021, 10:26:13 UTC |
| 0f0b55b | Dominik Kirst | 26 January 2021, 10:26:08 UTC | closed binZF proof | 26 January 2021, 10:26:08 UTC |
| a9e1a2f | Marc Hermes | 26 January 2021, 10:23:02 UTC | clear up in PA reduction | 26 January 2021, 10:23:02 UTC |
| 20a6c41 | Dominik Kirst | 26 January 2021, 10:14:23 UTC | one admit left | 26 January 2021, 10:14:23 UTC |
| cb90f97 | Dominik Kirst | 26 January 2021, 09:25:02 UTC | only morphism lemmas left | 26 January 2021, 09:25:02 UTC |
| c699f72 | Dominik Kirst | 26 January 2021, 08:56:04 UTC | proved first admit | 26 January 2021, 08:56:04 UTC |
| 0c3ed9f | Dominik Kirst | 25 January 2021, 20:20:46 UTC | Merge branch 'itp' of https://github.com/dominik-kirst/coq-library-undecidability into itp | 25 January 2021, 20:20:46 UTC |
| 7ee0371 | Dominik Kirst | 25 January 2021, 20:20:37 UTC | intensional verification to get rid of CE | 25 January 2021, 20:20:37 UTC |
| 140249f | Marc Hermes | 25 January 2021, 20:14:49 UTC | quick fix | 25 January 2021, 20:14:49 UTC |
| 5ca71b2 | Marc Hermes | 25 January 2021, 20:08:07 UTC | Version 2 done. Semantic part completed | 25 January 2021, 20:08:07 UTC |
| 4258f7e | Marc Hermes | 25 January 2021, 18:58:08 UTC | Merge branch 'itp' of https://github.com/dominik-kirst/coq-library-undecidability into itp | 25 January 2021, 18:58:08 UTC |
| 75f68a2 | Marc Hermes | 25 January 2021, 18:58:02 UTC | Version 1 of H10p to PA is done | 25 January 2021, 18:58:02 UTC |
| 5d5d1b8 | Dominik Kirst | 25 January 2021, 17:30:25 UTC | missing proof for vector lemma | 25 January 2021, 17:30:25 UTC |
| da1b2e1 | Dominik Kirst | 25 January 2021, 17:16:46 UTC | bounds tactic | 25 January 2021, 17:16:46 UTC |
| 7d453a9 | Marc Hermes | 25 January 2021, 16:15:01 UTC | push | 25 January 2021, 16:15:01 UTC |
| c5924bd | Marc Hermes | 25 January 2021, 14:18:38 UTC | quick fix | 25 January 2021, 14:18:38 UTC |
| ef8418b | Marc Hermes | 25 January 2021, 14:08:27 UTC | bounded_ext done | 25 January 2021, 14:08:27 UTC |
| fdaab85 | Marc Hermes | 25 January 2021, 14:06:02 UTC | bounded_ext done | 25 January 2021, 14:06:02 UTC |
| 3bc4a24 | Dominik Kirst | 25 January 2021, 12:40:17 UTC | changed implication notations | 25 January 2021, 12:40:17 UTC |
| 98e1bca | Dominik Kirst | 25 January 2021, 11:31:03 UTC | intensional model | 25 January 2021, 11:31:03 UTC |
| 680e7e7 | Marc Hermes | 24 January 2021, 18:39:29 UTC | added FA Utils | 24 January 2021, 18:39:29 UTC |
| 88e2d16 | Marc Hermes | 24 January 2021, 18:34:48 UTC | small fix | 24 January 2021, 18:34:48 UTC |
| 4271b77 | Dominik Kirst | 24 January 2021, 11:55:31 UTC | lemma structure for first half of translation | 24 January 2021, 11:55:31 UTC |
| 5e3c863 | Dominik Kirst | 23 January 2021, 14:18:40 UTC | closed admit | 23 January 2021, 14:18:40 UTC |
| 6fe2bc3 | Dominik Kirst | 23 January 2021, 13:46:07 UTC | bug fix | 23 January 2021, 13:46:07 UTC |
| 3252de0 | Marc Hermes | 23 January 2021, 10:54:53 UTC | added FA_facts | 23 January 2021, 10:54:53 UTC |
| 06da2fd | Dominik Kirst | 22 January 2021, 18:52:04 UTC | Z model and binary axiomatisation | 22 January 2021, 18:52:04 UTC |
| 9f2a368 | Marc Hermes | 22 January 2021, 17:50:59 UTC | added FA_facts | 22 January 2021, 17:50:59 UTC |
| d2b1c03 | Marc Hermes | 22 January 2021, 17:45:03 UTC | added FA_facts | 22 January 2021, 17:45:03 UTC |
| e5565db | Dominik Kirst | 22 January 2021, 12:15:59 UTC | H10 without parameters | 22 January 2021, 12:15:59 UTC |
| 2c39a9b | Dominik Kirst | 22 January 2021, 11:47:17 UTC | reformulated backwards direction | 22 January 2021, 11:47:17 UTC |
| 49a979a | Dominique Larchey-Wendling | 21 January 2021, 20:38:49 UTC | added direct reduction MMA2 --> ndMM2 w/o going through MM2 | 21 January 2021, 20:38:49 UTC |
| fa81e73 | Dominik Kirst | 21 January 2021, 17:10:46 UTC | little improvement | 21 January 2021, 17:10:46 UTC |
| 0899a02 | Dominik Kirst | 21 January 2021, 11:03:05 UTC | Merge branch 'itp' of https://github.com/dominik-kirst/coq-library-undecidability into itp | 21 January 2021, 11:03:05 UTC |
| b53c4cc | Dominik Kirst | 21 January 2021, 10:59:47 UTC | approximation lemma | 21 January 2021, 10:59:47 UTC |
| b147c90 | Marc Hermes | 21 January 2021, 10:37:37 UTC | added PA_undec | 21 January 2021, 10:37:37 UTC |
| 60321ae | Dominik Kirst | 20 January 2021, 17:20:39 UTC | little simplification of reduction function | 20 January 2021, 17:20:39 UTC |
| 113b213 | Marc Hermes | 17 January 2021, 20:49:14 UTC | added PA.v | 17 January 2021, 20:49:14 UTC |
| 4af82b3 | Yannick Forster | 13 January 2021, 16:34:01 UTC | Merge pull request #107 from dominik-kirst/axioms_omega Undecidability of ZF Set Theory | 13 January 2021, 16:34:01 UTC |
| 1c1b593 | Dominik Kirst | 13 January 2021, 16:30:02 UTC | readme entry | 13 January 2021, 16:30:02 UTC |
| bcc47a8 | Dominik Kirst | 13 January 2021, 10:08:12 UTC | scope for ZF syntax notations | 13 January 2021, 10:08:12 UTC |
| e1a9ba9 | Dominik Kirst | 12 January 2021, 17:04:56 UTC | doc, comments, file splits, reduction lemmas | 12 January 2021, 17:04:56 UTC |
| e0368f5 | Dominik Kirst | 04 January 2021, 08:47:23 UTC | erased print assumptions | 04 January 2021, 08:47:23 UTC |
| 75045ca | Dominik Kirst | 30 December 2020, 10:46:36 UTC | nameless equivalences and improved axiom verification | 30 December 2020, 10:46:36 UTC |
| 77b0224 | Dominik Kirst | 29 December 2020, 12:42:38 UTC | substitution weakening | 29 December 2020, 12:42:38 UTC |
| 0f093d4 | Dominik Kirst | 29 December 2020, 12:23:02 UTC | proved substitution induction principle | 29 December 2020, 12:23:02 UTC |
| f778d78 | Dominik Kirst | 29 December 2020, 11:35:47 UTC | restructuring | 29 December 2020, 11:35:47 UTC |
| 7ec062e | Dominik Kirst | 28 December 2020, 16:52:16 UTC | closed reductions to minimal signature | 28 December 2020, 16:52:16 UTC |
| dd6a10c | Dominik Kirst | 28 December 2020, 12:56:57 UTC | closed axiom verifications | 28 December 2020, 12:56:57 UTC |
| 8f77cd4 | Dominik Kirst | 28 December 2020, 11:27:02 UTC | modifying is_inductive | 28 December 2020, 11:27:02 UTC |
| f61d150 | Dominik Kirst | 28 December 2020, 10:55:16 UTC | proved second infinity axiom | 28 December 2020, 10:55:16 UTC |
| 06888e6 | Dominik Kirst | 27 December 2020, 15:27:27 UTC | verified all axioms but infinity | 27 December 2020, 15:27:27 UTC |
| a7c1897 | Dominik Kirst | 23 December 2020, 12:41:13 UTC | finished completeness | 23 December 2020, 12:41:13 UTC |
| eccd324 | Dominik Kirst | 23 December 2020, 09:09:13 UTC | only pair case missing in uniqueness | 23 December 2020, 09:09:13 UTC |
| a2f759b | Dominik Kirst | 22 December 2020, 18:02:30 UTC | proved Leibniz rule | 22 December 2020, 18:02:30 UTC |
| 8a37c9e | Dominik Kirst | 22 December 2020, 16:31:45 UTC | only internal deductions left | 22 December 2020, 16:31:45 UTC |
| a963444 | Dominik Kirst | 22 December 2020, 13:35:02 UTC | term existence and uniqueness missing | 22 December 2020, 13:35:02 UTC |
| b1d46a6 | Dominik Kirst | 21 December 2020, 17:01:39 UTC | structural lemmas | 21 December 2020, 17:01:39 UTC |
| c46caf9 | Dominik Kirst | 21 December 2020, 13:09:25 UTC | working on deduction direction | 21 December 2020, 13:09:25 UTC |
| 298e702 | Dominik Kirst | 21 December 2020, 11:52:06 UTC | cleanup | 21 December 2020, 11:52:06 UTC |
| 800a8dd | Dominik Kirst | 21 December 2020, 11:18:25 UTC | finished backwards proof | 21 December 2020, 11:18:25 UTC |
| f340fe1 | Dominik Kirst | 20 December 2020, 19:40:56 UTC | semantic embedding proof | 20 December 2020, 19:40:56 UTC |
| d8dcf5f | Dominique Larchey-Wendling | 17 December 2020, 14:40:29 UTC | removed an unused name in a pattern | 17 December 2020, 14:40:29 UTC |
| e6cf2ac | Yannick Forster | 15 December 2020, 08:03:17 UTC | Merge pull request #103 from mrhaandi/sr01 simple semi-Thue system 01 rewriting; cleanups | 15 December 2020, 08:03:17 UTC |
| 2cc66a4 | Andrej Dudenhefner | 14 December 2020, 13:27:52 UTC | added Set Default Goal Selector "!". | 14 December 2020, 13:27:52 UTC |
| bb9369f | Andrej Dudenhefner | 14 December 2020, 11:07:10 UTC | added README entry | 14 December 2020, 11:07:10 UTC |
| 5e6abc3 | Andrej Dudenhefner | 14 December 2020, 10:51:45 UTC | documentation | 14 December 2020, 10:51:45 UTC |
| 5edce60 | Andrej Dudenhefner | 14 December 2020, 10:41:38 UTC | removed Omega from HOU | 14 December 2020, 10:41:38 UTC |
| 0c45683 | Andrej Dudenhefner | 13 December 2020, 14:31:27 UTC | improved HOU compilation time | 13 December 2020, 17:46:54 UTC |
| 802e080 | Andrej Dudenhefner | 12 December 2020, 18:57:04 UTC | added CM2_HALT to CM1_HALT reduction | 13 December 2020, 14:15:37 UTC |
| 0ef8eef | Andrej Dudenhefner | 12 December 2020, 12:16:15 UTC | simplified SMNdl, FMSetC, LPolyNC, HSC | 12 December 2020, 14:39:06 UTC |
| efa5d5e | Andrej Dudenhefner | 12 December 2020, 10:02:03 UTC | simplified HSC proofs | 12 December 2020, 10:02:03 UTC |
| d78efa9 | Andrej Dudenhefner | 11 December 2020, 17:59:05 UTC | documentation, faster vos compilation | 11 December 2020, 18:16:21 UTC |
