Tree @master (Download .tar.gz)
Commit History
@master
git clone https://git.catseye.tc/Philomath/
- Arrange licensing info in repo according to REUSE 3.2 convention. Chris Pressey 2 months ago
- Update README. Chris Pressey 11 months ago
- Demo trying to manipulate formula after theorem has been built. Chris Pressey 11 months ago
- Merge branch 'master' into develop-2023.12xx Chris Pressey 11 months ago
- Add another example non-proof. Chris Pressey 11 months ago
- We don't actually need to protect assumptions; proof internals. Chris Pressey 11 months ago
- Clone (deep copy) formulas and assumptions when using them. Chris Pressey 11 months ago
- Improve the test driver script. Chris Pressey 11 months ago
- Move towards protecting the assumptions and formula in theorems. Chris Pressey 11 months ago
- Add a rudimentary test driver which is very rudimentary. Chris Pressey 11 months ago
- Update some links. Chris Pressey 11 months ago
- Merge pull request #1 from catseye/develop-202209xx Chris Pressey (commit: GitHub) 2 years ago
- Rename from "proof.c" to "theorem.c" because it defines theorems. Chris Pressey 2 years ago
- Fix typo in comment. Chris Pressey 2 years ago
- "struct theorem" is a better name than "struct proof" for this. Chris Pressey 2 years ago
- Add "see-also 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 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
- 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