Commit Graph

48 Commits

Author SHA1 Message Date
Fedor Isakov 27becb70a1 Fix the wording in fitch sample README 2018-08-19 17:32:59 +02:00
Fedor Isakov 98dfe30756 Resaved all models 2018-08-03 11:48:36 +02:00
Fedor Isakov d26805db7d Switch to the latest version of reactor lib 0.9.1 2018-08-03 11:48:36 +02:00
Fedor Isakov e2a68b4012 Fixes necessary for compatibility with MPS 2018.2 2018-07-22 16:51:10 +02:00
Fedor Isakov 7c1cb3b684 Name solutions and models consistently in samples (fitch) 2018-07-22 14:48:12 +02:00
Fedor Isakov 0bacffb611 Move type setting operation to typechecking lang. 2018-07-22 11:09:49 +02:00
Fedor Isakov 430b081085 Rename sandbox to demo solution in fitch sample. 2018-07-21 13:50:54 +02:00
Fedor Isakov c7cc97fffb Rename reporting runtim solution. 2018-07-21 13:29:40 +02:00
Fedor Isakov 6e00dcd58c Fix handler activating constraints declared elsewhere. 2018-07-21 13:29:40 +02:00
Fedor Isakov ea9919f38a Bring the hierarchy of DataForm concepts in line with the runtime.
Merge DataForm constructors into logic language.
Repackaging logic runtime.
Drop obsolete code.
2018-07-21 13:29:22 +02:00
Fedor Isakov 3791a3b216 Auto-updated descriptors. 2018-07-20 10:51:53 +02:00
Fedor Isakov 814baf4bce Update readme files. 2018-07-19 15:12:34 +02:00
Fedor Isakov e29a0576e2 Rename the root project and artifacts to "coderules". 2018-07-18 15:54:52 +02:00
Fedor Isakov d5b27ac6e2 Move sandbox solution to "solutions" folder. 2018-07-18 15:54:52 +02:00
Fedor Isakov e03cd48125 Add fitch sample to the common build. 2018-07-18 15:54:52 +02:00
Fedor Isakov 061e75f3f5 Auto-updated files after switching to the latest plugin. 2018-07-18 15:54:51 +02:00
Fedor Isakov 776ba9282b Re-save everything after switching to the newest typechecking plugin. 2018-07-18 15:54:51 +02:00
Fedor Isakov b87b71f07c Automatically migrated to the latest typechecking plugin. 2018-07-18 15:54:51 +02:00
Fedor Isakov 124cc3cd93 Switch to the latest typechecking plugin. Drop auto-triggering of checkAll constraint, use query instead. Switch to single stage. 2018-07-18 15:54:51 +02:00
Fedor Isakov adfae88953 Fix imports and establish extends relation among handlers. 2018-07-18 15:54:51 +02:00
Fedor Isakov 7107dce378 Applied the migration. 2018-07-18 15:54:51 +02:00
Fedor Isakov dc662b97b9 Convert to reporting expressions, drop obsolete constraints. 2018-07-18 15:54:51 +02:00
Fedor Isakov 9f1632b018 Updated to latest MPS and typechecking plugin. 2018-07-18 15:54:51 +02:00
Fedor Isakov 2aa168e32e Docs on Herbrand and First Order Logics 2018-07-18 15:54:51 +02:00
Fedor Isakov 72b2f0d110 Fix the Equality Introduction rule. 2018-07-18 15:54:51 +02:00
Fedor Isakov f070e7a34b Implementation of First Order logic. 2018-07-18 15:54:51 +02:00
Fedor Isakov 25d0238155 Implementation of Herbrand logic, an example. 2018-07-18 15:54:51 +02:00
Fedor Isakov 848df81dd4 Refactor out abstract proof, provide a mechanism to filter passing rules by the proof kind. 2018-07-18 15:54:51 +02:00
Fedor Isakov 5a550836b6 A couple of renamings to straighten the nomenclature. 2018-07-18 15:54:51 +02:00
Fedor Isakov 908e557d72 A language for Herbrand logic. 2018-07-18 15:54:51 +02:00
Fedor Isakov e3d2ac503b Move inference rules to propositional logic language. 2018-07-18 15:54:51 +02:00
Fedor Isakov e2ceb9b500 Some refactorings and renamings in preparation for intruduction of Herbrand logic language. 2018-07-18 15:54:50 +02:00
Fedor Isakov aa3837cd72 Separate logic-related stuff from proof-related. 2018-07-18 15:54:50 +02:00
Fedor Isakov 929a017704 Drop *_old stuff and the migration logs. 2018-07-18 15:54:50 +02:00
Fedor Isakov cd0e7cc1b1 Introduce a language for propositional logic. Move relevant stuff there. 2018-07-18 15:54:50 +02:00
Fedor Isakov 5353654e31 Migrate to MPS 2017.3. 2018-07-18 15:54:50 +02:00
Fedor Isakov db40250922 Proofread README file. 2018-07-18 15:54:50 +02:00
Fedor Isakov 1d272127f9 Update the instructions for installing the typechecking plugin. 2018-07-18 15:54:50 +02:00
Fedor Isakov 8683c18479 Completing the documentation. Fixed a sample. Some cosmetic improvements. 2018-07-18 15:54:50 +02:00
Fedor Isakov 197241d37d A few more samples. 2018-07-18 15:54:50 +02:00
Fedor Isakov 4a9b422acd Add README file. 2018-07-18 15:54:50 +02:00
Fedor Isakov 08350e6c68 Cosmetic changes, some comments. 2018-07-18 15:54:50 +02:00
Fedor Isakov 15d5a08bce Completing the typesystem (OrElim, IffIntro, IffElim). Another couple of samples. Fix the Reiteration editor. 2018-07-18 15:54:50 +02:00
Fedor Isakov 64c0318489 Completing the typesystem (IfElim, AndIntro, AndElim).
Basis for IfIntro is a SubProof.
Fix goal validation.
Editor fixes.
Another couple of samples.
2018-07-18 15:54:50 +02:00
Fedor Isakov b4f3ae1ef6 Introduce reiteration. Assumption to be used only as a subproof start. 2018-07-18 15:54:50 +02:00
Fedor Isakov 4c42629555 Rewritten the proof checker without the typeOf constraint, only assign type to the goal. 2018-07-18 15:54:50 +02:00
Fedor Isakov 784a1cedd0 Refactor "conclusion" out to Reasoning.
Add typechecking (incomplete).
Optimize the editor.
2018-07-18 15:54:50 +02:00
Fedor Isakov d09373eaa9 Initial import 2018-07-18 15:54:50 +02:00