git @ Cat's Eye Technologies Philomath / faef14f
Initial import of work so far. Chris Pressey 3 years ago
10 changed file(s) with 374 addition(s) and 0 deletion(s). Raw diff Collapse all Expand all
+2
-0
.gitignore less more
0 *.o
1
+52
-0
README.md less more
0 Philomath
1 =========
2
3 An LCF-style theorem prover written in ANSI C.
4
5 It implements a Natural Deduction system with labelled assumptions.
6 The rules of inference implement the intuitionistic propositional calculus.
7
8 How do I write a proof with this?
9 ---------------------------------
10
11 Create a file `eg/myproof.c`:
12
13 ```c
14 #include "formula.h"
15 #include "proof.h"
16 int main(int argc, char **argv) {
17 ...
18 }
19 ```
20
21 Then compile this:
22
23 ./build-proof eg/myproof
24
25 And run the resulting executable:
26
27 ./eg/myproof
28
29 If the exit code is 0, the proof is valid!
30
31 % echo $?
32 0
33
34 Progress
35 --------
36
37 - [x] conj_intro
38 - [x] conj_elim
39 - [x] impl_intro
40 - [x] impl_elim
41 - [x] disj_intro
42 - [x] disj_elim
43 - [ ] abs_elim: if abs is proved, then anything is proved
44 - [ ] neg_elim: if x is proved, and not x is proved, then absurdum is proved
45 - [ ] neg_intro: if gamma, phi proves absurdum, then gamma proves not phi
46
47 TODO
48 ----
49
50 * Demo proofs
51 * Cmd to build and run a demo proof
+6
-0
build.sh less more
0 #!/bin/sh -ex
1
2 CC="gcc -ansi -pedantic"
3 for MODULE in formula assumptions proof; do
4 (cd src && ${CC} -I../include -c $MODULE.c -o $MODULE.o)
5 done
+3
-0
clean.sh less more
0 #!/bin/sh -ex
1
2 rm -f src/*.o
+19
-0
include/assumptions.h less more
0 /* assumptions.h */
1
2 #ifndef ASSUMPTIONS_H
3 #define ASSUMPTIONS_H 1
4
5 #include "formula.h"
6
7 struct assumptions {
8 int label;
9 struct formula *formula;
10 struct assumptions *next;
11 };
12
13 struct assumptions *assume(int, struct formula *, struct assumptions *);
14 struct formula *lookup(int, struct assumptions *);
15 struct assumptions *discharge(int, struct assumptions *);
16 struct assumptions *merge(struct assumptions *, struct assumptions *);
17
18 #endif /* ndef ASSUMPTIONS_H */
+27
-0
include/formula.h less more
0 /* formula.h */
1
2 #ifndef FORMULA_H
3 #define FORMULA_H 1
4
5 #define VAR 0
6 #define CONJ 1
7 #define DISJ 2
8 #define IMPL 3
9 #define NEG 4
10
11 struct formula {
12 int type;
13 const char *name;
14 struct formula *lhs;
15 struct formula *rhs;
16 };
17
18 struct formula *var(const char *);
19 struct formula *conj(struct formula *, struct formula *);
20 struct formula *disj(struct formula *, struct formula *);
21 struct formula *impl(struct formula *, struct formula *);
22 struct formula *neg(struct formula *);
23
24 int formula_eq(struct formula *, struct formula *);
25
26 #endif /* ndef FORMULA_H */
+26
-0
include/proof.h less more
0 /* proof.h */
1
2 #ifndef PROOF_H
3 #define PROOF_H 1
4
5 #include "formula.h"
6
7 struct proof;
8
9 struct proof *suppose(struct formula *, int);
10
11 struct proof *conj_intro(struct proof *, struct proof *);
12 struct proof *conj_elim_lhs(struct proof *);
13 struct proof *conj_elim_rhs(struct proof *);
14
15 struct proof *impl_intro(int, struct proof *);
16 struct proof *impl_elim(struct proof *, struct proof *);
17
18 struct proof *disj_intro_lhs(struct formula *, struct proof *);
19 struct proof *disj_intro_rhs(struct proof *, struct formula *);
20 struct proof *disj_elim(struct proof *, struct proof *, int, struct proof *, int);
21
22 struct proof *conj_elim_lhs(struct proof *);
23 struct proof *conj_elim_rhs(struct proof *);
24
25 #endif /* ndef PROOF_H */
+60
-0
src/assumptions.c less more
0 #include <stdlib.h>
1 #include <stdio.h>
2
3 #include "formula.h"
4 #include "assumptions.h"
5
6 struct assumptions *
7 assume(int label, struct formula *formula, struct assumptions *next) {
8 struct assumptions *a = malloc(sizeof(struct assumptions));
9 a->label = label;
10 a->formula = formula;
11 a->next = next;
12 return a;
13 }
14
15 struct formula *
16 lookup(int label, struct assumptions *assumptions) {
17 struct assumptions *a = assumptions;
18 while (a != NULL) {
19 if (a->label == label) {
20 return a->formula;
21 }
22 a = a->next;
23 }
24 return NULL;
25 }
26
27 struct assumptions *
28 discharge(int label, struct assumptions *assumptions) {
29 /* Returns a copy of the assumptions, without
30 the assumption with the given label. */
31 struct assumptions *a = assumptions;
32 struct assumptions *result = NULL;
33 while (a != NULL) {
34 if (a->label != label) {
35 result = assume(a->label, a->formula, result);
36 }
37 a = a->next;
38 }
39 return result;
40 }
41
42 struct assumptions *
43 merge(struct assumptions *a, struct assumptions *b) {
44 struct assumptions *k = a;
45 struct assumptions *c = NULL;
46 struct formula *f;
47
48 while (k != NULL) {
49 f = lookup(k->label, b);
50 if (f == NULL || formula_eq(f, k->formula)) {
51 c = assume(k->label, k->formula, c);
52 } else {
53 fprintf(stderr, "Inconsistent assumptions with same label (%d)", k->label);
54 exit(1);
55 }
56 }
57
58 return c;
59 }
+58
-0
src/formula.c less more
0 #include <stdlib.h>
1
2 #include "formula.h"
3
4 struct formula *
5 mk_formula(int type, const char *name, struct formula *lhs, struct formula *rhs) {
6 struct formula *f = malloc(sizeof(struct formula));
7 f->type = type;
8 f->name = name;
9 f->lhs = lhs;
10 f->rhs = rhs;
11 return f;
12 }
13
14 struct formula *
15 var(const char *name) {
16 return mk_formula(VAR, name, NULL, NULL);
17 }
18
19 struct formula *
20 conj(struct formula *lhs, struct formula *rhs) {
21 return mk_formula(CONJ, NULL, lhs, rhs);
22 }
23
24 struct formula *
25 disj(struct formula *lhs, struct formula *rhs) {
26 return mk_formula(DISJ, NULL, lhs, rhs);
27 }
28
29 struct formula *
30 impl(struct formula *lhs, struct formula *rhs) {
31 return mk_formula(IMPL, NULL, lhs, rhs);
32 }
33
34 struct formula *
35 neg(struct formula *rhs) {
36 return mk_formula(NEG, NULL, NULL, rhs);
37 }
38
39 int
40 formula_eq(struct formula *a, struct formula *b) {
41 if (a == NULL && b == NULL) {
42 return 1;
43 }
44 if (a->type != b->type) {
45 return 0;
46 }
47 if (a->type == VAR && !strcmp(a->name, b->name)) {
48 return 1;
49 }
50 if (a->type == CONJ || a->type == DISJ || a->type == IMPL) {
51 return formula_eq(a->lhs, b->lhs) && formula_eq(a->rhs, b->rhs);
52 }
53 if (a->type == NEG) {
54 return formula_eq(a->rhs, b->rhs);
55 }
56 return 0;
57 }
+121
-0
src/proof.c less more
0 #include <stdlib.h>
1
2 #include "formula.h"
3 #include "assumptions.h"
4 #include "proof.h"
5
6 struct proof {
7 struct assumptions *assumptions;
8 struct formula *conclusion;
9 };
10
11 struct proof *
12 mk_proof(struct assumptions *assumptions, struct formula *conclusion) {
13 struct proof *p = malloc(sizeof(struct proof));
14 p->assumptions = assumptions;
15 p->conclusion = conclusion;
16 return p;
17 }
18
19 struct proof *
20 suppose(struct formula *formula, int label) {
21 return mk_proof(
22 assume(label, formula, NULL),
23 formula
24 );
25 }
26
27 struct proof *
28 conj_intro(struct proof *p, struct proof *q) {
29 /* If p is proved, and q is proved, then p & q is proved. */
30 return mk_proof(
31 merge(p->assumptions, q->assumptions),
32 conj(p->conclusion, q->conclusion)
33 );
34 }
35
36 struct proof *
37 conj_elim_lhs(struct proof *r) {
38 /* If r (of the form p & q) is proved, then p is proved. */
39 assert(r->conclusion->type == CONJ);
40 return mk_proof(
41 r->assumptions,
42 r->conclusion->lhs
43 );
44 }
45
46 struct proof *
47 conj_elim_rhs(struct proof *r) {
48 /* If r (of the form p & q) is proved, then q is proved. */
49 assert(r->conclusion->type == CONJ);
50 return mk_proof(
51 r->assumptions,
52 r->conclusion->rhs
53 );
54 }
55
56 struct proof *
57 impl_intro(int label, struct proof *q) {
58 /* If q is proved under the assumption p, then p -> q is proved. */
59 struct formula *f = lookup(label, q->assumptions);
60 struct assumptions *a = discharge(label, q->assumptions);
61 return mk_proof(
62 a,
63 impl(f, q->conclusion)
64 );
65 }
66
67 struct proof *
68 impl_elim(struct proof *p, struct proof *r) {
69 /* If p is proved, and r (of the form p -> q) is proved, then q is proved. */
70 assert(r->conclusion->type == IMPL);
71 assert(formula_eq(r->conclusion->lhs, p->conclusion));
72 return mk_proof(
73 merge(p->assumptions, r->assumptions),
74 r->conclusion->rhs
75 );
76 }
77
78 struct proof *
79 disj_intro_lhs(struct formula *p, struct proof *q) {
80 /* If q is proved, then p v q is proved, for any p. */
81 return mk_proof(
82 q->assumptions,
83 disj(p, q->conclusion)
84 );
85 }
86
87 struct proof *
88 disj_intro_rhs(struct proof *p, struct formula *q) {
89 /* If p is proved, then p v q is proved, for any q. */
90 return mk_proof(
91 p->assumptions,
92 disj(p->conclusion, q)
93 );
94 }
95
96 struct proof *
97 disj_elim(struct proof *r, struct proof *s, int label1, struct proof *t, int label2) {
98 /* If r is proved, and under the assumption labelled "1" s is proved, and under
99 the assumption labelled "2" t is proved, and s concludes the same as t,
100 and r is proved and r is in the form "1" v "2", then s is proved. */
101 struct formula *f1, *f2;
102 struct assumptions *a_s, *a_t;
103
104 assert(r->conclusion->type == DISJ);
105
106 f1 = lookup(label1, s->assumptions);
107 a_s = discharge(label2, s->assumptions);
108
109 f2 = lookup(label2, t->assumptions);
110 a_t = discharge(label2, t->assumptions);
111
112 assert(formula_eq(s->conclusion, t->conclusion));
113 assert(formula_eq(r->conclusion->lhs, f1));
114 assert(formula_eq(r->conclusion->rhs, f2));
115
116 return mk_proof(
117 merge(r->assumptions, merge(a_s, a_t)),
118 s->conclusion
119 );
120 }