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

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

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

Move towards protecting the assumptions and formula in theorems.
Chris Pressey
6 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

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

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

Fix bug in disj_elim(). Add demo of disj_intro(), disj_elim().
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

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

Initial import of work so far.
Chris Pressey
2 years ago