"Progress" is done, replace with a "To do" section.
Chris Pressey
1 year, 3 months ago
| 57 | 57 | Fortunately, it is possible to statically analyze a C source file and confirm |
| 58 | 58 | that it does none of these things, if such a level of assurance is desired. |
| 59 | 59 | |
| 60 | Progress | |
| 61 | -------- | |
| 60 | TODO | |
| 61 | ---- | |
| 62 | 62 | |
| 63 | - [x] assert() | |
| 64 | - [x] proves() | |
| 63 | Should really have more demo non-proofs, to check that it's not | |
| 64 | letting non-proofs pass themselves off as proofs. | |
| 65 | 65 | |
| 66 | - [x] impl_intro | |
| 67 | - [x] demo proof showing impl_intro | |
| 68 | - [x] impl_elim | |
| 69 | - [x] demo proof showing impl_elim | |
| 70 | ||
| 71 | - [x] conj_intro | |
| 72 | - [x] demo proof showing conj_intro | |
| 73 | - [x] conj_elim | |
| 74 | - [x] demo proof showing conj_elim | |
| 75 | ||
| 76 | - [x] disj_intro | |
| 77 | - [x] demo proof showing disj_intro | |
| 78 | - [x] disj_elim | |
| 79 | - [x] demo proof showing disj_elim | |
| 80 | ||
| 81 | - [x] demo bad proof (ought to really be a number of these) | |
| 82 | - [x] debug flag for (or debug version of) `build-proof.sh` | |
| 83 | ||
| 84 | - [x] Use some names other than p, q, etc for struct proof type args | |
| 85 | ||
| 86 | - [x] Absurdum value | |
| 87 | - [x] absr_elim: if absurdum is proved, then anything is proved (absr |- phi) | |
| 88 | - [x] demo proof showing absr_elim | |
| 89 | - [x] neg_elim: if x is proved, and not x is proved, then absurdum is proved (phi, not phi |- absr) | |
| 90 | - [x] demo proof showing neg_elim | |
| 91 | - [x] neg_intro: if gamma, phi proves absurdum, then gamma proves not phi (gamma |- not phi, discharging gamma, phi) | |
| 92 | - [x] demo proof showing neg_intro | |
| 93 | ||
| 94 | - [x] double_neg_elim (for to support classical logic) | |
| 95 | - [x] demo proof showing double_neg_elim | |
| 66 | Could stand to have a real suite of unit tests instead of just | |
| 67 | a handful of demo proofs than you can build and run manually. | |
| 96 | 68 | |
| 97 | 69 | [classical propositional logic]: https://iep.utm.edu/natural-deduction/#H4 |
| 98 | 70 | [Natural Deduction]: https://iep.utm.edu/natural-deduction/ |