```    1:- module(lin_refute, []).    2:- use_module(util('fol-cnf')).    3:- op(1050, xfy, <-).    4
5% ?- forall(invalid_formula(A), prove_test(A)).
6prove_test(A):- writeln(A), prove(A), !, writeln(valid), nl.
7prove_test(_):- writeln(invalid), nl.
8
9
10% ?- spy(solve).
11% ?- F = (all(x, p(x)->p(f(x)))-> (p(d)->p(f(f(f(d)))))),
12%	prove_test(F).
13% ?- F = (all(x, p(x)->p(f(x)))-> (p(d)->p(g(d)))),
14%	prove_test(F).
15% ?- F = (all(x, p(x)->p(f(x)))-> (p(d)->p(f(g(f(d)))))),
16%	prove_test(F).
17% ?- F = (all(x, p(x)->(p(f(x))*p(g(x))))-> (p(d)->p(f(g(f(d)))))),
18%	prove_test(F).
19
20% ?- forall(valid_formula(_A), prove_test(_A)).
21valid_formula((-(-a) -> a) * (a -> -(-a))).		% Double Negation
22valid_formula( ((a * b) -> -((-a + -b))) * (-((-a + -b)) -> (a * b))). % De Morganâs Law
23valid_formula( (-b -> f) * ((b *f) -> -i) * ((i + -b) -> -f) -> b).
24valid_formula(a + -a).
25valid_formula(((a -> b) -> a) -> a).  % Peirceâs Law
26valid_formula(-(-a)->a).
27valid_formula(a -> a).
28valid_formula(a -> (b -> a)).
29valid_formula((a->b)->((b->c)->(a->c))).
30valid_formula(a->((a->b)->b)).
31valid_formula((a*(a->b))->b).
32valid_formula((a->b)->(-b -> -a)).
33valid_formula((a->b)->((b->c)->(a->c))).
34valid_formula((((((((p3== p2) == p1) == p0) == p3) == p2) == p1) == p0)).
35valid_formula(all(x, p==a(x))==(p==all(x, a(x)))).
36valid_formula(all(y, p==f(y))==(p==all(x, f(x)))).
37valid_formula(all(x, p== f(x)) == (p==all(x, f(x)))).
38valid_formula(all(x, p== f(x))== (p==all(x, f(x)))).
39valid_formula(all(x, p== f(x)) -> (p==all(x, f(x)))).
40valid_formula(all(x, p-> f(x)) <- (p==all(x, f(x)))).
41valid_formula((p->all(x, f(x)))-> all(x, p->f(x))).
42valid_formula((p==all(x, f(x)))-> all(x, f(x)->p)).
43valid_formula((p->all(x, q(x) * -q(x)))-> all(x, ((q(x)* -q(x))->p))).
44valid_formula(((p* -p)->all(x, q(x) * -q(x)))-> all(x, ((q(x)* -q(x))->(p* -p)))).
45
46% ?- forall(invalid_formula(_A), prove_test(_A)).
47invalid_formula(a).
48invalid_formula((a->b)->a).
49invalid_formula((a->b)->(b->a)).
50invalid_formula(a -> (b -> c)).
51invalid_formula( (-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f)).
52invalid_formula( -((-b -> f) * ((b * f) -> -i) * ((i + -b) -> -f) -> (i * f))).
53invalid_formula(-(p->all(x, f(x))); all(x, f(x)->p)).
54invalid_formula(-( -p;all(x, f(x))); all(x, f(x)->p)).
55invalid_formula( p * some(x, -f(x)); all(x, -f(x)| p)).
56invalid_formula( p * some(x, -f(x)); all(x, -f(x))).
57invalid_formula( p * -f(a); all(x, -f(x))).
58invalid_formula( -f(a) ; all(x, -f(x))).
59invalid_formula( -f(a) + all(x, -f(x))).
60invalid_formula(all(x, p<- f(x)) <- (p<-all(x, f(x)))).
61invalid_formula(all(x, p<- f(x)) <- (p==all(x, f(x)))).
62
63		/***********************
64		*     Linear Solver    *
65		***********************/
66
67% ?- prove(a).
68% ?- prove((a->b)->a).
69% ?- prove((a->b)->(b->a)).
70% ?- prove(a->(b->c)).
71% ?- prove(a*(a->b)->b).
72% ?- prove(a->(b->a)).
73% ?- prove((a+b)->(a->c)->(b->c)->c).
74% ?- prove(forall(X, p(X)->q(X))*p(a)-> p(a)).
75% ?- prove(forall(X, p(X)->q(X)) -> (p(a)-> p(a))).
76prove(FOL):- prove_by_refutation(FOL).
77%
78prove_by_refutation(FOL):- fol_cnf(-FOL, CNF), refute_cnf(CNF).
79%
80complementary(-P, P):-!.
81complementary(P, -P).
82
86
89	(	variant(X, Y) -> fail
90	; 	R = [Y|Zs],
92	).
93
94% ?- complementary_free([a,b]).
95% ?- complementary_free([a,-b]).
96% ?- complementary_free([a,-a, b]).
97complementary_free([]).
98complementary_free([_]).
99complementary_free([X, Y|Z]):- complementary(X, X0),
100	X0\==Y,
101	complementary_free([Y|Z]).
102
103% ?- binary_resolvent([a], [-a], R).
104% ?- binary_resolvent([a,b], [-a,c], R).
105binary_resolvent([X|Xs], C, R):-
106	complementary(X, X0),
107	copy_term(C, C0),
108	select(Y, C0, C1),
109	unify_with_occurs_check(X0, Y),
110	append(Xs, C1, D),
111	cls_sort(D, R).
112
113% ?- binary_resolvent_chk([a], [-a], R).
114% ?- binary_resolvent_chk([a,b], [-a,-b, c], R).
115binary_resolvent_chk(Xs, C, R):- binary_resolvent(Xs, C, R),
116	complementary_free(R).
117
118		/*****************************
119		*     iterative deepening    *
120		*****************************/
121
122% ?- fol_cnf((a+b)->c, CNF).
123% ?- refute_cnf([[a],[-a]]).
124% ?- refute_cnf([[a],[a]]).
125% ?- refute_cnf([[a,b],[-a],[-b]]).
126% ?- refute_cnf([[a,b],[-a],[b]]).
127% ?- CNF=[[-b], [b, f], [b, -f], [-f, -i], [-b, -f, -i]], refute_cnf(CNF).
128% ?- CNF=[[-b], [b, f], [b, -f]], refute_cnf(CNF).
129refute_cnf(CNF):- solve_with_depth_limit(CNF, 2, f(0)).
130
131%
132solve_with_depth_limit(CNF, M, R):-
133	select(C, CNF, CNF0),
134	solve(C, [], CNF0, [], 0, M, R),
135	arg(1, R, 0),
136	!.
137solve_with_depth_limit(CNF, M, R):- arg(1, R, 1),
138	 M0 is 2*M,
139	 nb_setarg(1, R, 0),
140	 solve_with_depth_limit(CNF, M0, R).
141
142%
143solve([], _, _, _, _, _, _):-!.
144solve([X|Xs], As, CNF, History, I, M, R):-
145	complementary(X, X0),
146	(	I > M ->
147		nb_setarg(1, R, 1),
148		fail
149	;	member(D, As),
150		(	X0 == D			% ancestor resolution
151		;	X == D			% tabling ?
152		),
153		J = I,
154		solve(Xs, As, CNF, History, J, M, R)
155	; 	member(D, CNF),
156		copy_term(D, D0),
157		select(Y, D0, D1),
158		unify_with_occurs_check(X0, Y),
159		append(D1, Xs, Ys),
160		cls_sort(Ys, Zs),
161		complementary_free(Zs),
162		J is I + 1,
163		cls_sort([Y|As], Bs),