Commit Graph

1301 Commits

Author SHA1 Message Date
Fedor Isakov 0a76533f33 Fix paths to images. 2018-07-19 15:17:06 +02:00
Fedor Isakov 814baf4bce Update readme files. 2018-07-19 15:12:34 +02:00
Fedor Isakov 1c33ddca9a Configure the dependency on conreactor to be resolved through local maven repo. Make travis install reactor libs locally. 2018-07-19 10:52:03 +02:00
Fedor Isakov c92b8a616c Import 'conreactor' project and its history as a subproject. 2018-07-18 16:49: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
Fedor Isakov 0d4d61d5f9 Change the sample project name to lambdacalc. 2018-07-18 15:54:50 +02:00
Fedor Isakov 78a0601625 Include lambdacalc sample into the common build. 2018-07-18 15:54:50 +02:00
Fedor Isakov 95d836df85 Auto-update after switching to the latest plugin. 2018-07-18 15:54:49 +02:00
Fedor Isakov 7ae9c936a6 Re-save everything after switching to the newest typechecking plugin. 2018-07-18 15:54:49 +02:00
Fedor Isakov 4e669b5412 Automatically migrated to the latest typechecking plugin. Drop second stage. 2018-07-18 15:54:49 +02:00
Fedor Isakov f6121832a7 Switch to the latest typechecking plugin. Introduce Typecheck query. Drop automatic activation of "recoverAll". 2018-07-18 15:54:49 +02:00
Fedor Isakov 08beb2ce13 Drop usages of a deprecated concept, replace with custom constraint. Fix imports. 2018-07-18 15:54:49 +02:00
Fedor Isakov 67ebe51be1 Applied the migration. 2018-07-18 15:54:49 +02:00
Fedor Isakov e140342a4c Replace custom constraints with reporting operations. 2018-07-18 15:54:49 +02:00
Fedor Isakov 2e3cb6278c Migrated to the latest MPS release and typechecking plugin. 2018-07-18 15:54:49 +02:00