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

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

Fix typo in comment.
Chris Pressey
1 year, 16 days ago

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

Use less confusing (maybe) parameter names x, y, z for input proofs.
Chris Pressey
1 year, 3 months ago

Implement double_neg_elim. Demo proof of reductio ad absurdum.
Chris Pressey
1 year, 3 months ago

Implement neg_intro().
Chris Pressey
1 year, 3 months ago

Find and fix a bug in neg_elim. Add `D` option to buildproof.sh.
Chris Pressey
1 year, 3 months ago

Implementation of neg_elim() (untested).
Chris Pressey
1 year, 5 months ago

Absurdum terms, and absr_elim() rule.
Chris Pressey
1 year, 5 months ago

Fix bug in disj_elim(). Add demo of disj_intro(), disj_elim().
Chris Pressey
1 year, 5 months ago

Remove debugging of assumptions in impl_elim.
Chris Pressey
1 year, 5 months ago

Fix algorithm for merging assumptions.
Chris Pressey
1 year, 5 months ago

Add debugging prints. merge() assumptions doesn't work, it seems.
Chris Pressey
1 year, 5 months ago

assumptions_fprint().
Chris Pressey
1 year, 5 months ago

formula_fprint().
Chris Pressey
1 year, 5 months ago

Have assert() display a diagnostic message.
Chris Pressey
1 year, 5 months ago

Basic version of proves(), needs debugging.
Chris Pressey
1 year, 5 months ago

assert.{c,h}. Fix linkedlist traversal bug in merge().
Chris Pressey
1 year, 6 months ago

Initial import of work so far.
Chris Pressey
1 year, 6 months ago