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
|
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
|
d5b27ac6e2
|
Move sandbox solution to "solutions" folder.
|
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
|
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
|
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
|
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 |