| f13f2ce | Mario Carneiro | 23 February 2023, 17:26:04 UTC | add files for ITP 2023 submission | 23 February 2023, 17:26:04 UTC |
| c320e05 | Mario Carneiro | 23 February 2023, 08:31:13 UTC | more readme | 23 February 2023, 08:31:13 UTC |
| b1eb24b | Mario Carneiro | 23 February 2023, 08:16:25 UTC | reproducible build, add README | 23 February 2023, 08:16:25 UTC |
| 059491c | Mario Carneiro | 22 February 2023, 10:35:10 UTC | Add GPLv3 license This is a derivative of the GPL licensed Mizar project (https://github.com/MizarProject/system), hence it is also GPL licensed. | 22 February 2023, 10:35:10 UTC |
| 8eb4aa6 | Mario Carneiro | 22 February 2023, 10:28:45 UTC | tweaks | 22 February 2023, 10:28:45 UTC |
| 9b7f73b | Mario Carneiro | 19 February 2023, 07:30:24 UTC | debugging analyzer: file 8 | 19 February 2023, 07:30:24 UTC |
| 7f48d65 | Mario Carneiro | 18 February 2023, 06:07:22 UTC | debugging analyzer: file 2 | 18 February 2023, 06:07:22 UTC |
| eec3b74 | Mario Carneiro | 17 February 2023, 23:33:35 UTC | debugging analyzer: file 0 | 17 February 2023, 23:33:35 UTC |
| dd06465 | Mario Carneiro | 16 February 2023, 21:33:09 UTC | re-bugfix the checker since we added a bunch of stuff and in particular changed FlexAnd handling. Unfortunately it's not all roses, we now have a real unsoundness in the checker which cannot be fixed without breaking MML. | 16 February 2023, 21:33:34 UTC |
| e7d0d3f | Mario Carneiro | 15 February 2023, 11:09:34 UTC | Analyzer part 13: flex-and elaboration (and we're done!) | 15 February 2023, 11:09:34 UTC |
| 4655c8b | Mario Carneiro | 15 February 2023, 08:05:31 UTC | change FlexAnd representation I was planning to do this eventually anyway, but it turns out that the existing representation actually has a soundness bug, in addition to the sketchy unpacking code in `expand()`, because it is not true that equality of the endpoints implies equality of the FlexAnd expressions. For example, `P[1+1] /\ ... /\ P[n]` represents `P[x]` for `x in 1..=n` but if you substitute `n = 2+2` then you get the expression `P[1+1] /\ ... /\ P[2+2]`, which if re-parsed actually results in `P[x+x]` for `x in 1..=2`. These two expressions are not equivalent despite having the same endpoints and this can be used to prove false. | 15 February 2023, 08:08:39 UTC |
| f498ae7 | Mario Carneiro | 15 February 2023, 04:43:37 UTC | Analyzer part 12: properties | 15 February 2023, 04:43:37 UTC |
| 106d58b | Mario Carneiro | 12 February 2023, 07:51:33 UTC | Analyzer part 11: notations (synonym/antonym) | 12 February 2023, 07:51:33 UTC |
| 6fd75cc | Mario Carneiro | 11 February 2023, 16:10:03 UTC | Analyzer part 10.6: sethood registrations | 11 February 2023, 16:10:03 UTC |
| aca18d1 | Mario Carneiro | 11 February 2023, 15:46:53 UTC | Analyzer part 10.5: reduction registrations | 11 February 2023, 15:46:53 UTC |
| 4bf7dd4 | Mario Carneiro | 11 February 2023, 14:20:30 UTC | Analyzer part 10.4: identify registrations | 11 February 2023, 14:20:30 UTC |
| 1260a3d | Mario Carneiro | 06 February 2023, 11:06:09 UTC | Analyzer part 10.3: conditional registrations | 06 February 2023, 11:06:09 UTC |
| 8ffcb29 | Mario Carneiro | 06 February 2023, 10:30:49 UTC | Analyzer part 10.2: functor registration | 06 February 2023, 10:30:49 UTC |
| 5e328be | Mario Carneiro | 06 February 2023, 08:43:53 UTC | Analyzer part 10.1: existential cluster registration | 06 February 2023, 08:43:53 UTC |
| 20a541f | Mario Carneiro | 06 February 2023, 05:55:57 UTC | Analyzer part 9: structure definitions | 06 February 2023, 05:55:57 UTC |
| 37f81fc | Mario Carneiro | 30 January 2023, 05:20:13 UTC | extract functions | 30 January 2023, 05:20:13 UTC |
| cf046b8 | Mario Carneiro | 30 January 2023, 05:11:28 UTC | Analyzer part 8.6: functor definitions | 30 January 2023, 05:11:28 UTC |
| 0d08008 | Mario Carneiro | 30 January 2023, 03:32:50 UTC | Analyzer part 8.5: attribute definitions | 30 January 2023, 03:32:50 UTC |
| 062b034 | Mario Carneiro | 30 January 2023, 01:57:27 UTC | Analyzer part 8.4: predicate definitions | 30 January 2023, 01:57:27 UTC |
| 855dad0 | Mario Carneiro | 29 January 2023, 23:43:37 UTC | Analyzer part 8.3: expandable mode definitions | 29 January 2023, 23:43:37 UTC |
| f6be949 | Mario Carneiro | 29 January 2023, 23:13:59 UTC | Analyzer part 8.2: mode redefinitions | 29 January 2023, 23:13:59 UTC |
| d6a47f2 | Mario Carneiro | 29 January 2023, 14:48:25 UTC | Analyzer part 8.1: mode definitions | 29 January 2023, 14:48:25 UTC |
| 4103d8d | Mario Carneiro | 24 January 2023, 22:15:36 UTC | Analyzer part 7: non-proof block structure | 24 January 2023, 22:15:36 UTC |
| e6d8e30 | Mario Carneiro | 18 January 2023, 23:48:40 UTC | Analyzer part 6: inferences | 19 January 2023, 00:25:22 UTC |
| 886d060 | Mario Carneiro | 18 January 2023, 23:31:55 UTC | Analyzer part 5: private statements | 19 January 2023, 00:24:53 UTC |
| f81a3d0 | Mario Carneiro | 18 January 2023, 21:37:32 UTC | Analyzer part 4: WHNF, proof skeleton steps | 18 January 2023, 21:37:32 UTC |
| 8d5a91f | Mario Carneiro | 18 January 2023, 12:33:24 UTC | Analyzer part 3: thesis reconstruction | 18 January 2023, 12:33:24 UTC |
| deda160 | Mario Carneiro | 17 January 2023, 00:52:43 UTC | Analyzer part 2: proof skeleton steps | 17 January 2023, 00:53:52 UTC |
| 58ca6c1 | Mario Carneiro | 13 January 2023, 13:33:13 UTC | Analyzer part 1: elaborating terms/types/formulas | 13 January 2023, 13:33:13 UTC |
| 75154b3 | Mario Carneiro | 13 January 2023, 13:26:54 UTC | allow borrowed expressions in Subst | 13 January 2023, 13:27:47 UTC |
| d923403 | Mario Carneiro | 13 January 2023, 13:16:09 UTC | move run_checker() to reader | 13 January 2023, 13:17:11 UTC |
| f2b60c8 | Mario Carneiro | 13 January 2023, 13:08:11 UTC | MSM refactoring | 13 January 2023, 13:11:31 UTC |
| dc8b2fb | Mario Carneiro | 13 January 2023, 12:30:01 UTC | move `recursive_round_up` to a parameter | 13 January 2023, 12:31:30 UTC |
| a6b3ada | Mario Carneiro | 10 January 2023, 14:44:53 UTC | refactoring + renaming | 10 January 2023, 14:50:32 UTC |
| dade45b | Mario Carneiro | 10 January 2023, 14:02:38 UTC | testing and bugfixing the MSM parser | 10 January 2023, 14:02:38 UTC |
| b37924a | Mario Carneiro | 09 January 2023, 21:01:42 UTC | Add MSM/WSM parser | 10 January 2023, 07:37:34 UTC |
| 6b76e17 | Mario Carneiro | 09 January 2023, 20:56:19 UTC | refactoring the parser | 10 January 2023, 07:37:34 UTC |
| befe8f0 | Mario Carneiro | 08 January 2023, 08:23:00 UTC | unused code cleanup | 08 January 2023, 08:23:00 UTC |
| cd35d3c | Mario Carneiro | 07 January 2023, 17:57:37 UTC | parallelize the checker Thanks to care taken earlier to not use global variables like mizar does, we can trivially parallelize the checker. | 08 January 2023, 01:28:46 UTC |
| 269d4c3 | Mario Carneiro | 07 January 2023, 17:54:52 UTC | MML 100% checked! This implements the linear arithmetic module, which was the last remaining piece of the checker. We can now check every single proof in the MML. | 08 January 2023, 01:28:46 UTC |
| 0919e91 | Mario Carneiro | 06 January 2023, 12:11:41 UTC | bigger bignums I tried to just use 64 bits but unfortunately this fails on only one proof in the MML. So we do a proper bignum implementation this time, with a small num optimization because the vast majority of numbers in the MML are small. We also remove the error recovery for overflow, both because it is now much less likely and also because treating them as opaque constants on overflow is just a roundabout way to get proof failures. | 06 January 2023, 12:11:41 UTC |
| 34a797f | Mario Carneiro | 06 January 2023, 10:29:52 UTC | Bugfixing round 2 We now compile error-free on MML again, but this time without skipping half of all theorems because they have numbers in them. Results: bignum: 177 linear: 168590 success: 1820821 So we are at 91% checking. Notably we have achieved 100% of schematizer proofs. What remains are a handful of proofs that need bigger bignums, and linear arithmetic. | 06 January 2023, 10:29:52 UTC |
| 95acff1 | Mario Carneiro | 03 January 2023, 08:56:11 UTC | Equalizer part 6: bignum, polynomial arithmetic For now the bignums are actually fixed size - we'll see whether this causes failures in the MML. | 03 January 2023, 08:56:11 UTC |
| f4f9d55 | Mario Carneiro | 03 January 2023, 08:49:29 UTC | Add schematizer This is a lot more straightforward than the other parts. | 03 January 2023, 08:49:29 UTC |
| 31e9dfa | Mario Carneiro | 30 December 2022, 19:18:32 UTC | numeric evaluation in equate | 30 December 2022, 19:18:32 UTC |
| 6d950a8 | Mario Carneiro | 30 December 2022, 03:50:29 UTC | basic support for numeric evaluation (outside equate) | 30 December 2022, 03:50:29 UTC |
| c34ac1a | Mario Carneiro | 30 December 2022, 01:51:22 UTC | Success! MML checked, modulo skipped proofs and `from` The breakdown of remaining work: from: 13026 numbers: 727008 success: 726038 | 30 December 2022, 01:51:22 UTC |
| c825180 | Mario Carneiro | 29 December 2022, 08:32:24 UTC | error recovery from lattice overflow Apparently there are proofs in the MML which actually take advantage of the fact that the checker recovers from a lattice overflow to try instantiating a different quantifier, so we have to make sure to catch overflow errors. I hope the 6000 limit is applied in the right places.. | 29 December 2022, 08:32:24 UTC |
| 5e10b15 | Mario Carneiro | 29 December 2022, 07:39:39 UTC | basic implementation of numeral recognition only enough to make 1 != 2 provable | 29 December 2022, 07:39:39 UTC |
| e213de2 | Mario Carneiro | 28 December 2022, 07:23:00 UTC | somehow this whole function evaded the first 400 files | 28 December 2022, 07:23:00 UTC |
| fdcbf4c | Mario Carneiro | 28 December 2022, 05:32:23 UTC | the bugs will continue until morale improves | 28 December 2022, 05:32:23 UTC |
| dd48bb5 | Mario Carneiro | 28 December 2022, 05:30:59 UTC | formatter improvements | 28 December 2022, 05:30:59 UTC |
| d8f8d27 | Mario Carneiro | 27 December 2022, 03:19:28 UTC | turns out round_up_type is order-dependent | 27 December 2022, 03:19:28 UTC |
| f964b4d | Mario Carneiro | 26 December 2022, 17:22:20 UTC | refactor visitors, more format options, bugfixes | 26 December 2022, 22:29:22 UTC |
| 45255f6 | Mario Carneiro | 25 December 2022, 20:44:04 UTC | better documentation on requirements | 25 December 2022, 20:44:04 UTC |
| 0fab174 | Mario Carneiro | 25 December 2022, 15:14:56 UTC | some renames | 25 December 2022, 20:43:40 UTC |
| c4f8aac | Mario Carneiro | 25 December 2022, 08:01:14 UTC | lots of bugfixes (success up to file 82!) | 25 December 2022, 08:01:14 UTC |
| ad850f6 | Mario Carneiro | 24 December 2022, 07:31:00 UTC | Unifier part 4: resolution We now have all the core elements of the mizar 'by' checker, and TARSKI can be 100% verified. Let's celebrate for now and debug next. | 24 December 2022, 07:42:48 UTC |
| 232aad4 | Mario Carneiro | 24 December 2022, 03:42:29 UTC | more bugfixing (close to parity with `verifier -u` now) | 24 December 2022, 03:42:29 UTC |
| 6f4c20a | Mario Carneiro | 23 December 2022, 04:11:51 UTC | improve formatter | 23 December 2022, 04:11:51 UTC |
| c161b78 | Mario Carneiro | 23 December 2022, 04:11:01 UTC | testing & bugfixing | 23 December 2022, 04:11:01 UTC |
| de52c5d | Mario Carneiro | 23 December 2022, 01:12:14 UTC | Unifier part 3: building substitution constraints | 23 December 2022, 01:12:14 UTC |
| 5295dd6 | Mario Carneiro | 19 December 2022, 07:12:42 UTC | Unifier part 2: falsify (with comments) because the negations are enough to make your head spin | 19 December 2022, 07:12:42 UTC |
| f443cad | Mario Carneiro | 18 December 2022, 23:49:36 UTC | Unifier part 1: main unify function | 18 December 2022, 23:49:36 UTC |
| f0aae10 | Mario Carneiro | 18 December 2022, 20:10:41 UTC | Pre-unification pass | 18 December 2022, 20:10:41 UTC |
| 42c4568 | Mario Carneiro | 18 December 2022, 00:26:45 UTC | equalizer bugfixes, improve formatter | 18 December 2022, 18:12:25 UTC |
| 4c17352 | Mario Carneiro | 16 December 2022, 20:01:28 UTC | Add pretty printer Why is pretty printing mizar so stupidly complicated? Gah! | 16 December 2022, 20:01:28 UTC |
| b30c1d5 | Mario Carneiro | 16 December 2022, 01:45:29 UTC | finish equalizer, clean up | 16 December 2022, 01:53:40 UTC |
| a17e5ff | Mario Carneiro | 16 December 2022, 01:38:45 UTC | Equalizer part 5: rounding up superclusters | 16 December 2022, 01:38:45 UTC |
| 400801a | Mario Carneiro | 15 December 2022, 22:39:14 UTC | Equalizer part 4: theory reasoning | 15 December 2022, 22:39:14 UTC |
| 38148ed | Mario Carneiro | 15 December 2022, 05:29:12 UTC | Equalizer part 3: YYTerm, Identities | 15 December 2022, 05:29:12 UTC |
| dacb928 | Mario Carneiro | 14 December 2022, 00:53:58 UTC | Equalizer part 2: process reductions | 14 December 2022, 00:53:58 UTC |
| 19b7dd0 | Mario Carneiro | 09 December 2022, 16:13:42 UTC | Equalizer part 1: Y pass | 09 December 2022, 16:13:42 UTC |
| c57d751 | Mario Carneiro | 07 December 2022, 10:35:50 UTC | finished the prechecker (untested) | 08 December 2022, 10:26:14 UTC |
| 4d19138 | Mario Carneiro | 05 December 2022, 15:17:22 UTC | finished article processing modulo by/from, works on MML | 05 December 2022, 15:17:22 UTC |
| ec5f6e4 | Mario Carneiro | 02 December 2022, 14:22:15 UTC | initial commit | 02 December 2022, 14:22:15 UTC |
