Commit 3f4a98ec849d2ae5f9681155f3ac55b436167002 - Philomath

+5

-1

README.md less more

34	34
35	35	% echo $?
36	36	0
	37
	38	If you wish to build the proof with debugging output, you can pass the `-D` flag:
	39
	40	./build-proof.sh -D myproof
37	41
38	42	Limitations
39	43	-----------

75	79	- [x] demo proof showing disj_elim
76	80
77	81	- [x] demo bad proof (ought to really be a number of these)
78		- [ ] debug flag for (or debug version of) `build-proof.sh`
	82	- [x] debug flag for (or debug version of) `build-proof.sh`
79	83
80	84	- [ ] Use names of greek letters for arguments to the functions
81	85

+6

-1

build-proof.sh less more

0	0	#!/bin/sh -ex
1	1
2		./build.sh
	2	CFLAGS=""
	3	if [ "x$1" = "x-D" ]; then
	4	CFLAGS="-DDEBUG"
	5	shift
	6	fi
	7	CFLAGS=${CFLAGS} ./build.sh
3	8	PROOF=$1
4	9	CC="gcc -ansi -pedantic"
5	10	${CC} -Iinclude $PROOF.c src/*.o -o $PROOF.exe

+1

-1

build.sh less more

1	1
2	2	CC="gcc -ansi -pedantic"
3	3	for MODULE in assert formula assumptions proof; do
4		(cd src && ${CC} -I../include -c $MODULE.c -o $MODULE.o)
	4	(cd src && ${CC} ${CFLAGS} -I../include -c $MODULE.c -o $MODULE.o)
5	5	done

+13

-8

eg/demo-proof4.c less more

11	11	* Hence, p -> q by (3)
12	12	* Now, suppose q (4)
13	13	* Further, suppose p (5)
14		* Hence, p -> q by (5)
	14	* Hence, p -> q by (5) -- FIXME
15	15	* So, p -> q by disj_elim with (2), (4)
16	16	* So, ~p \/ q -> (p -> q) by (1)
17	17	*/

20	20	#include "proof.h"
21	21
22	22	int main(int argc, char **argv) {
23		struct proof *step1 = suppose(disj(neg(var("p")), var("q")), 1);
24		struct proof *step2 = suppose(neg(var("p")), 2);
25		struct proof *step3 = suppose(var("p"), 3);
26		struct proof *step4 = neg_elim(step3, step2);
27		/* ... TODO ... */
28		struct proof *step99 = impl_intro(1, step1);
	23	struct proof step1 = suppose(disj(neg(var("p")), var("q")), 1); / Suppose ~p \/ q (1) */
	24	struct proof step2 = suppose(neg(var("p")), 2); / Now, suppose ~p (2) */
	25	struct proof step3 = suppose(var("p"), 3); / Further, suppose p (3) */
	26	struct proof step4 = neg_elim(step3, step2); / So bottom, by neg_elim */
	27	struct proof step5 = absr_elim(step4, var("q")); / Hence q, by absr_elim */
	28	struct proof step6 = impl_intro(3, step5); / Hence, p -> q by (3) */
	29	struct proof step7 = suppose(var("q"), 4); / Now, suppose q (4) */
	30	struct proof step8 = suppose(var("p"), 5); / Further, suppose p (5) */
	31	struct proof step9 = impl_intro(5, step8); / Hence, p -> q by (5) */
	32	/* ... TODO ... / / So, p -> q by disj_elim with (2), (4) */
	33	/* ... TODO ... / / So, ~p \/ q -> (p -> q) by (1) */
29	34
30	35	return proves(
31		step99,
	36	step1,
32	37	impl(disj(neg(var("p")), var("q")), impl(var("p"), var("q")))
33	38	);
34	39	}

+8

-1

src/proof.c less more

88	88	/* If q is proved under the assumption p, then p -> q is proved. */
89	89	struct formula *f = lookup(label, q->assumptions);
90	90	struct assumptions *a = discharge(label, q->assumptions);
	91	#ifdef DEBUG
	92	if (f == NULL) {
	93	fprintf(stdout, "Label %d not found in:", label);
	94	assumptions_fprint(stdout, a);
	95	fprintf(stdout, "\n");
	96	}
	97	#endif
91	98	assert(f != NULL, "impl_intro: label not found in assumptions");
92	99	return mk_proof(
93	100	a,

164	171	neg_elim(struct proof p, struct proof q)
165	172	{
166	173	assert(q->conclusion->type == NEG, "neg_elim: not a negation");
167		assert(formula_eq(p->conclusion, q->conclusion->lhs), "neg_elim: mismatched conclusions");
	174	assert(formula_eq(p->conclusion, q->conclusion->rhs), "neg_elim: mismatched conclusions");
168	175	return mk_proof(
169	176	merge(p->assumptions, q->assumptions),
170	177	absr()