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

• Arrange licensing info in repo according to REUSE 3.2 convention. Chris Pressey 3 months ago
• Demo trying to manipulate formula after theorem has been built. Chris Pressey 1 year, 7 days ago
• Add another example non-proof. Chris Pressey 1 year, 7 days ago
• "struct theorem" is a better name than "struct proof" for this. Chris Pressey 2 years ago
• Implement double_neg_elim. Demo proof of reductio ad absurdum. 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
• Fix bug in disj_elim(). Add demo of disj_intro(), disj_elim(). Chris Pressey 2 years ago
• Example of conj_{intro,elim}. Improve build-proof.sh. Update README. Chris Pressey 2 years ago
• Basic version of proves(), needs debugging. Chris Pressey 2 years ago
• assert.{c,h}. Fix linked-list traversal bug in merge(). Chris Pressey 2 years ago
• Example proof, script to build it; not quite complete yet though. Chris Pressey 2 years ago