| 4ddcbda | Richard Moot | 16 March 2015, 19:10:44 UTC | Commented out natural deduction | 16 March 2015, 19:10:44 UTC |
| 69c039c | Richard Moot | 16 March 2015, 16:17:43 UTC | Started natural deduction output | 16 March 2015, 16:17:43 UTC |
| 9821d9a | Richard Moot | 16 March 2015, 15:23:35 UTC | Added support for "+" and epsilon | 16 March 2015, 15:23:35 UTC |
| c9b78d5 | Richard Moot | 16 March 2015, 11:13:57 UTC | Corrected error | 16 March 2015, 11:13:57 UTC |
| 48d9b12 | Richard Moot | 16 March 2015, 09:02:50 UTC | Cut elimination seems to work More testing needed before merging in the master branch, but I may be getting close | 16 March 2015, 09:02:50 UTC |
| bc0f382 | Richard Moot | 16 March 2015, 01:29:07 UTC | Minor code cleanup | 16 March 2015, 01:29:07 UTC |
| b195881 | Richard Moot | 16 March 2015, 01:21:21 UTC | Close to a solution; cut for axioms and R-o seem to work | 16 March 2015, 01:21:21 UTC |
| 817a4bf | Richard Moot | 16 March 2015, 01:04:05 UTC | Changed axioms to be only half instantiated | 16 March 2015, 01:04:05 UTC |
| 559c12b | Richard Moot | 15 March 2015, 21:20:52 UTC | Testing left-ward cut elimination | 15 March 2015, 21:20:52 UTC |
| 290fe27 | Richard Moot | 15 March 2015, 16:32:59 UTC | Simple but important correction | 15 March 2015, 16:32:59 UTC |
| 86510b0 | Richard Moot | 15 March 2015, 15:40:12 UTC | Corrected error and added diagnostics | 15 March 2015, 15:40:12 UTC |
| 0dacca4 | Richard Moot | 15 March 2015, 14:55:55 UTC | Some progress on cut elimination | 15 March 2015, 14:55:55 UTC |
| 8f4b774 | Richard Moot | 15 March 2015, 01:32:31 UTC | Minor corrections | 15 March 2015, 01:32:31 UTC |
| 89fc41e | Richard Moot | 15 March 2015, 01:10:32 UTC | Work on cut elimination Added preliminary versions of left-ward moving and right-ward moving cut elimination | 15 March 2015, 01:10:32 UTC |
| 2db4456 | Richard Moot | 14 March 2015, 22:59:57 UTC | Comments | 14 March 2015, 22:59:57 UTC |
| 0db9b3b | Richard Moot | 14 March 2015, 22:48:14 UTC | Started split of cut-elimination | 14 March 2015, 22:48:14 UTC |
| 40ef015 | Richard Moot | 14 March 2015, 21:03:37 UTC | Added comments | 14 March 2015, 21:03:37 UTC |
| d01deba | Richard Moot | 13 March 2015, 22:00:02 UTC | Merged in some master edits | 13 March 2015, 22:00:02 UTC |
| d64d17c | Richard Moot | 13 March 2015, 19:20:56 UTC | Some modification | 13 March 2015, 19:20:56 UTC |
| cb6a861 | Richard Moot | 13 March 2015, 15:48:14 UTC | updated pos_proof | 13 March 2015, 15:48:14 UTC |
| 4d06e68 | Richard Moot | 13 March 2015, 11:49:00 UTC | Simplified/commented | 13 March 2015, 11:49:00 UTC |
| c8376c0 | Richard Moot | 13 March 2015, 00:59:06 UTC | Some progress, needs more testing | 13 March 2015, 00:59:06 UTC |
| f8894f6 | Richard Moot | 12 March 2015, 21:52:42 UTC | Code cleanup | 12 March 2015, 21:52:42 UTC |
| 7e597d9 | Richard Moot | 12 March 2015, 19:40:01 UTC | Corrected error in lexicon-less semantics | 12 March 2015, 19:40:01 UTC |
| b3172a0 | Richard Moot | 12 March 2015, 14:53:45 UTC | Added sequent statistics to unfolding | 12 March 2015, 14:53:45 UTC |
| 08e2257 | Richard Moot | 12 March 2015, 14:19:38 UTC | Corrected error | 12 March 2015, 14:19:38 UTC |
| 339b16b | Richard Moot | 12 March 2015, 12:27:51 UTC | Correction to proof generation | 12 March 2015, 12:27:51 UTC |
| ef454b8 | Richard Moot | 12 March 2015, 01:26:51 UTC | Added forall/exists/iota to latex_atom | 12 March 2015, 01:26:51 UTC |
| 8c636f1 | Richard Moot | 11 March 2015, 21:18:06 UTC | Correction to proof generation Also: added extra non-pied-piping case to d_grammar | 11 March 2015, 21:18:06 UTC |
| c67ed40 | Richard Moot | 11 March 2015, 20:37:28 UTC | Subtle but important changes to proof generation With a bit of luck, I may have resolved the issue with variables. Further testing necessary. | 11 March 2015, 20:37:28 UTC |
| a622d22 | Richard Moot | 11 March 2015, 17:04:41 UTC | Minor modifications | 11 March 2015, 17:04:41 UTC |
| a9cebd9 | Richard Moot | 11 March 2015, 16:34:10 UTC | Cleanup | 11 March 2015, 16:34:10 UTC |
| 655162c | Richard Moot | 11 March 2015, 16:15:59 UTC | Updated Makefile and tarball | 11 March 2015, 16:15:59 UTC |
| aecc68f | Richard Moot | 11 March 2015, 16:11:24 UTC | Comments/cleanup The parse and parse_all predicates have been move from lexicon.pl to the main file (much more natural; it is now with the rest of the top-level predicates) | 11 March 2015, 16:11:24 UTC |
| 3cfb8e1 | Richard Moot | 11 March 2015, 15:13:34 UTC | Factorisation | 11 March 2015, 15:13:34 UTC |
| 9f7ff80 | Richard Moot | 11 March 2015, 14:38:58 UTC | Code factorisation Moved boring replacement predicates to a separate module. | 11 March 2015, 14:38:58 UTC |
| bdf1475 | Richard Moot | 11 March 2015, 13:53:54 UTC | Minor additions | 11 March 2015, 13:53:54 UTC |
| de215d0 | Richard Moot | 11 March 2015, 12:21:53 UTC | Merged edits | 11 March 2015, 12:21:53 UTC |
| 92ab83c | Richard Moot | 11 March 2015, 10:58:27 UTC | Minor addition to unary_term/1 | 11 March 2015, 10:58:27 UTC |
| 9779c8d | Richard Moot | 11 March 2015, 10:49:37 UTC | Typeset semantics as (left numbered) equations | 11 March 2015, 10:49:37 UTC |
| 5541be4 | Richard Moot | 11 March 2015, 09:26:04 UTC | Added Polymnie support | 11 March 2015, 09:26:04 UTC |
| 792dcd6 | Richard Moot | 11 March 2015, 08:47:59 UTC | Made some more brackets implicit | 11 March 2015, 08:47:59 UTC |
| 3921d79 | Richard Moot | 11 March 2015, 08:38:17 UTC | Removed conflicts from merge | 11 March 2015, 08:38:17 UTC |
| 0541d30 | Richard Moot | 11 March 2015, 01:07:36 UTC | Minor edit | 11 March 2015, 01:07:36 UTC |
| 091da1e | Richard Moot | 11 March 2015, 01:00:58 UTC | Merge branch 'master' into dancing-links Conflicts: mill1.pl | 11 March 2015, 01:00:58 UTC |
| 32aa50a | Richard Moot | 11 March 2015, 00:56:47 UTC | Merged dancing links | 11 March 2015, 00:56:47 UTC |
| 88e3d89 | Richard Moot | 11 March 2015, 00:52:25 UTC | Some cleaning up | 11 March 2015, 00:52:25 UTC |
| 0c9e567 | Richard Moot | 10 March 2015, 22:12:25 UTC | Another bugfix | 10 March 2015, 22:12:25 UTC |
| c19dbf4 | Richard Moot | 10 March 2015, 19:47:40 UTC | Debugging... | 10 March 2015, 19:47:40 UTC |
| 22bc82b | Richard Moot | 10 March 2015, 18:12:35 UTC | Some corrections | 10 March 2015, 18:12:35 UTC |
| 65373dc | Richard Moot | 10 March 2015, 17:55:49 UTC | Corrections Proof generation fails now, need to verify | 10 March 2015, 17:55:49 UTC |
| 466f4f5 | Richard Moot | 10 March 2015, 17:36:32 UTC | First attempt integrating dancing links with main code | 10 March 2015, 17:36:32 UTC |
| f166416 | Richard Moot | 10 March 2015, 15:25:31 UTC | First version of best axiom computation | 10 March 2015, 15:25:31 UTC |
| fef6a64 | Richard Moot | 10 March 2015, 12:23:20 UTC | Cleanup and improvement to atom colletion | 10 March 2015, 12:23:20 UTC |
| 8c654e6 | Richard Moot | 10 March 2015, 01:21:08 UTC | Minor code cleanup | 10 March 2015, 01:21:08 UTC |
| a82f9bc | Richard Moot | 10 March 2015, 00:57:06 UTC | Started programming dancing links | 10 March 2015, 00:57:06 UTC |
| 328c1ee | Richard Moot | 10 March 2015, 00:53:38 UTC | Merge pull request #5 from RichardMoot/dancing-links Minor changes | 10 March 2015, 00:53:38 UTC |
| 528ca8d | Richard Moot | 10 March 2015, 00:40:09 UTC | Minor changes | 10 March 2015, 00:40:09 UTC |
| 4842317 | Richard Moot | 09 March 2015, 14:52:20 UTC | Minor improvements to latex.pl | 09 March 2015, 14:52:20 UTC |
| 667f5a9 | Richard Moot | 09 March 2015, 13:42:44 UTC | Corrected proof generation Seems robust now, needs more intensive testing | 09 March 2015, 13:42:44 UTC |
| 9a4c84b | Richard Moot | 09 March 2015, 13:42:07 UTC | More warnings | 09 March 2015, 13:42:07 UTC |
| d5a9598 | Richard Moot | 09 March 2015, 08:54:26 UTC | Added abolish declarations To avoid interference from previously loaded grammar files, all grammar predicates are abolished. | 09 March 2015, 08:54:26 UTC |
| 7d91bfb | Richard Moot | 09 March 2015, 00:37:19 UTC | Cleanup and minor additions | 09 March 2015, 00:37:19 UTC |
| a393d55 | Richard Moot | 09 March 2015, 00:37:00 UTC | Added warning message for unknown terms (instead of failing silently | 09 March 2015, 00:37:00 UTC |
| 39f0b4a | Richard Moot | 08 March 2015, 16:39:57 UTC | Added type-raised quantifier analysis as alternative to split scope | 08 March 2015, 16:39:57 UTC |
| d19f95e | Richard Moot | 08 March 2015, 16:39:00 UTC | Added more useful debugging information and error messages | 08 March 2015, 16:39:00 UTC |
| 9c5325c | Richard Moot | 08 March 2015, 01:31:15 UTC | Added new example | 08 March 2015, 01:31:15 UTC |
| 8a0fe27 | Richard Moot | 07 March 2015, 19:56:29 UTC | Some extra hybrid grammar features | 07 March 2015, 19:56:29 UTC |
| e0fc389 | Richard Moot | 07 March 2015, 19:19:44 UTC | Added negation/necessity/possibility | 07 March 2015, 19:19:44 UTC |
| 866207b | Richard Moot | 07 March 2015, 19:19:20 UTC | Added many more examples | 07 March 2015, 19:19:20 UTC |
| 3d84c81 | Richard Moot | 07 March 2015, 16:16:21 UTC | Updated parse_all summary | 07 March 2015, 16:16:21 UTC |
| d8e0fef | Richard Moot | 07 March 2015, 15:37:14 UTC | Added parse_all predicate | 07 March 2015, 15:37:14 UTC |
| cad2218 | Richard Moot | 07 March 2015, 15:21:12 UTC | Minor corrections | 07 March 2015, 15:21:12 UTC |
| 38c013d | Richard Moot | 07 March 2015, 13:43:44 UTC | Refactored main prover predicates | 07 March 2015, 13:43:44 UTC |
| 866cc57 | Richard Moot | 07 March 2015, 13:43:25 UTC | Minor correction | 07 March 2015, 13:43:25 UTC |
| f3fd2e8 | Richard Moot | 06 March 2015, 16:48:52 UTC | Correction | 06 March 2015, 16:48:52 UTC |
| d0c60df | Richard Moot | 06 March 2015, 15:39:16 UTC | Added final reflexive examples | 06 March 2015, 15:39:16 UTC |
| 4da5643 | Richard Moot | 06 March 2015, 15:30:19 UTC | First (more or less) complete D grammar | 06 March 2015, 15:30:19 UTC |
| 91d53c0 | Richard Moot | 06 March 2015, 11:32:56 UTC | Corrected "gave the cold shoulder example" | 06 March 2015, 11:32:56 UTC |
| 97881c5 | Richard Moot | 06 March 2015, 01:42:48 UTC | Added \iota to semantics | 06 March 2015, 01:42:48 UTC |
| 0ee0523 | Richard Moot | 06 March 2015, 01:42:34 UTC | Corrected Dutch examples | 06 March 2015, 01:42:34 UTC |
| 9970446 | Richard Moot | 05 March 2015, 21:29:37 UTC | Corrections and new Dutch entries | 05 March 2015, 21:29:37 UTC |
| 1684329 | Richard Moot | 05 March 2015, 20:28:48 UTC | Added D grammar Added a D grammar, plus some new definitions to ease their development. New translation cases (and sort calculation) for bridge, lproj and rproj | 05 March 2015, 20:28:48 UTC |
| 6d8fb93 | Richard Moot | 05 March 2015, 00:34:42 UTC | Minor corrections | 05 March 2015, 00:34:42 UTC |
| b614e81 | Richard Moot | 04 March 2015, 17:16:51 UTC | prove/2 now subsumed by prove/3 | 04 March 2015, 17:16:51 UTC |
| fa7426a | Richard Moot | 04 March 2015, 17:16:24 UTC | Added pairing/projection | 04 March 2015, 17:16:24 UTC |
| b7d99b8 | Richard Moot | 04 March 2015, 17:04:22 UTC | First version of lexicon and latex semantics | 04 March 2015, 17:04:22 UTC |
| f92cfbb | Richard Moot | 04 March 2015, 15:36:21 UTC | Variable name corrections Looking good this time, but needs more verification. | 04 March 2015, 15:36:21 UTC |
| 45cd493 | Richard Moot | 04 March 2015, 14:51:28 UTC | Work on proof generation | 04 March 2015, 14:51:28 UTC |
| e67cee2 | Richard Moot | 04 March 2015, 11:13:09 UTC | Updated variable handling | 04 March 2015, 11:13:09 UTC |
| 5a51da6 | Richard Moot | 03 March 2015, 21:38:56 UTC | ISO Prolog I/O Updated graph/proof output to use iso I/O | 03 March 2015, 21:38:56 UTC |
| a2194b1 | Richard Moot | 03 March 2015, 18:12:23 UTC | Minor corrections/additions | 03 March 2015, 18:12:23 UTC |
| ecd4163 | Richard Moot | 03 March 2015, 17:12:27 UTC | Started work on lexicon | 03 March 2015, 17:12:27 UTC |
| 2b79f82 | Richard Moot | 03 March 2015, 16:19:28 UTC | Resolved variable names issue The variable names issue (where quantified variables were either portrayed using their instantiated version or unnecessarily renamed) seems to have been resolved. | 03 March 2015, 16:19:28 UTC |
| cd1dbfd | Richard Moot | 03 March 2015, 12:14:07 UTC | Update to rename_bound_variables | 03 March 2015, 12:14:07 UTC |
| 1a57c7b | Richard Moot | 03 March 2015, 00:50:40 UTC | Minor cleanup | 03 March 2015, 00:50:40 UTC |
| fee12cf | Richard Moot | 02 March 2015, 20:36:07 UTC | Bugfix | 02 March 2015, 20:36:07 UTC |
| 4c0a828 | Richard Moot | 02 March 2015, 16:26:56 UTC | Added hybrid/lambda example | 02 March 2015, 16:26:56 UTC |
| c498d06 | Richard Moot | 02 March 2015, 16:00:42 UTC | Corrections and bug fixes Need to verify test3(X), which has a problem with variables. | 02 March 2015, 16:00:42 UTC |
| 990cd6a | Richard Moot | 02 March 2015, 13:59:34 UTC | First complete LaTeX proofs First version of LaTeX proof output. Needs a lot more testing. | 02 March 2015, 13:59:34 UTC |
