Commit History
@master
git clone https://git.catseye.tc/Philomath/
-
Arrange licensing info in repo according to REUSE 3.2 convention.
Chris Pressey
5 months ago
-
Update README.
Chris Pressey
1 year, 1 month ago
-
Demo trying to manipulate formula after theorem has been built.
Chris Pressey
1 year, 1 month ago
-
Merge branch 'master' into develop-2023.12xx
Chris Pressey
1 year, 1 month ago
-
Add another example non-proof.
Chris Pressey
1 year, 1 month ago
-
We don't actually need to protect assumptions; proof internals.
Chris Pressey
1 year, 1 month ago
-
Clone (deep copy) formulas and assumptions when using them.
Chris Pressey
1 year, 1 month ago
-
Improve the test driver script.
Chris Pressey
1 year, 1 month ago
-
Move towards protecting the assumptions and formula in theorems.
Chris Pressey
1 year, 1 month ago
-
Add a rudimentary test driver which is very rudimentary.
Chris Pressey
1 year, 1 month ago
-
Update some links.
Chris Pressey
1 year, 1 month ago
-
Merge pull request #1 from catseye/develop-202209xx
Chris Pressey
(commit: GitHub)
2 years ago
-
Rename from "proof.c" to "theorem.c" because it defines theorems.
Chris Pressey
2 years ago
-
Fix typo in comment.
Chris Pressey
2 years ago
-
"struct theorem" is a better name than "struct proof" for this.
Chris Pressey
2 years ago
-
Add "see-also bar" to top of README.
Chris Pressey
2 years ago
-
Add UNLICENSE.
Chris Pressey
2 years ago
-
"Progress" is done, replace with a "To do" section.
Chris Pressey
2 years ago
-
Use less confusing (maybe) parameter names x, y, z for input proofs.
Chris Pressey
2 years ago
-
Implement double_neg_elim. Demo proof of reductio ad absurdum.
Chris Pressey
2 years ago
-
Implement neg_intro().
Chris Pressey
2 years ago
-
Finish the proof by simulating the copy rule with conj-intro-elim.
Chris Pressey
2 years ago
-
Find and fix a bug in neg_elim. Add `-D` option to build-proof.sh.
Chris Pressey
2 years ago
-
Checkpoint an incomplete proof that exercises neg_elim, absr_elim.
Chris Pressey
2 years ago
-
Demonstrate that we do in fact reject incorrectly formed proofs.
Chris Pressey
2 years ago
-
Implementation of neg_elim() (untested).
Chris Pressey
2 years ago
-
Absurdum terms, and absr_elim() rule.
Chris Pressey
2 years ago
-
Add notes to README.
Chris Pressey
2 years ago
-
Fix bug in disj_elim(). Add demo of disj_intro(), disj_elim().
Chris Pressey
2 years ago
-
Fix link.
Chris Pressey
2 years ago