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

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

Example of conj_{intro,elim}. Improve buildproof.sh. Update README.
Chris Pressey
2 years ago

Remove debugging of assumptions in impl_elim.
Chris Pressey
2 years ago

Fix algorithm for merging assumptions.
Chris Pressey
2 years ago

Add debugging prints. merge() assumptions doesn't work, it seems.
Chris Pressey
2 years ago

assumptions_fprint().
Chris Pressey
2 years ago

formula_fprint().
Chris Pressey
2 years ago

Have assert() display a diagnostic message.
Chris Pressey
2 years ago

Basic version of proves(), needs debugging.
Chris Pressey
2 years ago

Update README.
Chris Pressey
2 years ago

assert.{c,h}. Fix linkedlist traversal bug in merge().
Chris Pressey
2 years ago