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 |