History of
eg
@master
git clone https://git.catseye.tc/Philomath/
-
Demo trying to manipulate formula after theorem has been built.
Chris Pressey
4 months ago
-
Add another example non-proof.
Chris Pressey
4 months ago
-
"struct theorem" is a better name than "struct proof" for this.
Chris Pressey
1 year, 7 months ago
-
Implement double_neg_elim. Demo proof of reductio ad absurdum.
Chris Pressey
1 year, 10 months ago
-
Finish the proof by simulating the copy rule with conj-intro-elim.
Chris Pressey
1 year, 10 months ago
-
Find and fix a bug in neg_elim. Add `-D` option to build-proof.sh.
Chris Pressey
1 year, 11 months ago
-
Checkpoint an incomplete proof that exercises neg_elim, absr_elim.
Chris Pressey
1 year, 11 months ago
-
Demonstrate that we do in fact reject incorrectly formed proofs.
Chris Pressey
1 year, 11 months ago
-
Fix bug in disj_elim(). Add demo of disj_intro(), disj_elim().
Chris Pressey
2 years ago
-
Example of conj_{intro,elim}. Improve build-proof.sh. Update README.
Chris Pressey
2 years ago
-
Basic version of proves(), needs debugging.
Chris Pressey
2 years ago
-
assert.{c,h}. Fix linked-list traversal bug in merge().
Chris Pressey
2 years ago
-
Example proof, script to build it; not quite complete yet though.
Chris Pressey
2 years ago