Commit History
@master
git clone https://git.catseye.tc/Philomath/

Update README.
Chris Pressey
7 months ago

Demo trying to manipulate formula after theorem has been built.
Chris Pressey
7 months ago

Merge branch 'master' into develop2023.12xx
Chris Pressey
7 months ago

Add another example nonproof.
Chris Pressey
7 months ago

We don't actually need to protect assumptions; proof internals.
Chris Pressey
7 months ago

Clone (deep copy) formulas and assumptions when using them.
Chris Pressey
7 months ago

Improve the test driver script.
Chris Pressey
7 months ago

Move towards protecting the assumptions and formula in theorems.
Chris Pressey
7 months ago

Add a rudimentary test driver which is very rudimentary.
Chris Pressey
7 months ago

Update some links.
Chris Pressey
7 months ago

Merge pull request #1 from catseye/develop202209xx
Chris Pressey
(commit: GitHub)
1 year, 10 months ago

Rename from "proof.c" to "theorem.c" because it defines theorems.
Chris Pressey
1 year, 10 months ago

Fix typo in comment.
Chris Pressey
1 year, 10 months ago

"struct theorem" is a better name than "struct proof" for this.
Chris Pressey
1 year, 10 months ago

Add "seealso 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 conjintroelim.
Chris Pressey
2 years ago

Find and fix a bug in neg_elim. Add `D` option to buildproof.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

A few improvements and corrections to the README.
Chris Pressey
2 years ago