Demonstrate that we do in fact reject incorrectly formed proofs.
Chris Pressey
3 years ago
| 74 | 74 |
- [x] disj_elim
|
| 75 | 75 |
- [x] demo proof showing disj_elim
|
| 76 | 76 |
|
| 77 | |
- [ ] demo bad proof (ought to really be a number of these)
|
|
77 |
- [x] demo bad proof (ought to really be a number of these)
|
| 78 | 78 |
- [ ] debug flag for (or debug version of) `build-proof.sh`
|
| 79 | 79 |
|
| 80 | 80 |
- [ ] Use names of greek letters for arguments to the functions
|
|
0 |
/*
|
|
1 |
* Attempt to write a proof showing
|
|
2 |
* (p -> q) -> p
|
|
3 |
* but demonstrate that we do not allow that.
|
|
4 |
*/
|
|
5 |
|
|
6 |
#include "formula.h"
|
|
7 |
#include "proof.h"
|
|
8 |
|
|
9 |
int main(int argc, char **argv) {
|
|
10 |
return proves(
|
|
11 |
impl_intro(
|
|
12 |
1,
|
|
13 |
suppose(conj(var("p"), var("q")), 1)
|
|
14 |
),
|
|
15 |
impl(impl(var("p"), var("q")), var("p"))
|
|
16 |
);
|
|
17 |
}
|