```    1:- module(fol, [prove/2, prove/3]).    2
3:- use_module(pac('expand-pac')).    4:- include(pac(op)).    5term_expansion --> expand_pac.
6
7:- current_op(P, T, (->)), member(T,[xfy, yfx, xfx]), op(P, T, '<-').    8:- current_op(P, T, (->)), member(T,[xfy, yfx, xfx]), op(P, T, '<--').    9:- current_op(P, T, (->)), member(T,[xfy, yfx, xfx]), op(P, T, '<-->').   10:- current_op(P, T, (->)), member(T,[xfy, yfx, xfx]), op(P, T, '<->').   11
12%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
13% A simple but complete theorem prover based on     %
14% linear  resolution using iterated  deepening      %
15% search method.			            %
16%						    %
17%   by K.Mukai 1993 July / 2006 July, rewritten.    %
18%	2012 June  front end updated to PAC-based.  %
19%	2015 March main part rewritten.		    %
20%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
21
22		/**********************************
23		*     prove_by_linear_ancestor    *
24		**********************************/
25
26% ?- module(pac).
27% ?- trace, fol:prove(a->a, S).
28% ?- trace, fol:prove(a, S).
29% ?- F = ~((c; a;b)&(c; -a;b)&(c; a; -b)&(c; -a; -b)& (-c; a;b)&(-c; -a;b)&(-c; a; -b)&(-c; -a; -b)), prove(F, R, [trace(T)]),maplist(writeln, T).
30
31% ?-  F = [[append([],X,X)], [append([X|Y],Z,[X|U]), ~append(Y,Z,U)]], fol:prove(F, S, [center([[~append([a,b], U, [a,b,c,d,e])]]), initial_depth(300), clausal(true), iteration_limit(5)]).
32% ?- F = ~((a;b)&(-a;b)&(a; -b)&(-a; -b)), prove(F, R, [trace(X)]).
33%@ F = (~ ((a;b)& (-a;b)& (a;-b)& (-a;-b))),
34%@ R = 11,
35%@ X = [input_resolution([a, b], [b, ~a]), input_resolution([b], [a, ~b]), input_resolution([a], [~a, ~b]), ancestor_resolution([~b], [b])].
36
37prove(X, S):- once(prove(X, S, [])).
38
39%
40prove(X, S, Options):-
41	completing_options([center([]), initial_depth(300), iteration_limit(5)],
42			   Options, Options0),
43	memberchk(initial_depth(D), Options0),
44	memberchk(iteration_limit(N), Options0),
45	memberchk(center(SOS),  Options0),
46	(  is_list(X)
47	->	Y = X				% a set of clauses given.
48	; 	once(preprocess(~(X), Y))	% first-order formula given.
49	),
50	setup_input_clauses(Y, Y0),
51	once(( memberchk(trace(Trace), Options0); true )),
52	once((	Y0 == [],
53		S = 'The input has been reduced to empty set.',
54		Trace = []
55	; 	memberchk([], Y0),
56		S = 'proved.',
57		Trace = []
58	;	is_list(SOS),
59		SOS \== [],
60		iterated_deepening(
61			(	member(C0, SOS),
62				linear_prove(C0, [], Trace, [])),
63			   D, N, S)
64	; 	iterated_deepening(
65			(	input_clause(C0),
66				linear_prove(C0, [], Trace, [])),
67			   D, N, S)
68	;	S = 'no proof found.',
69		Trace = []
70	)).
71
72%
73setup_input_clauses(Y, Y3):-
74	maplist(merge_clause, Y, U),
75	merge_cnf(U, Y0),
76	sort(Y0, Y1),
77	pure_literal_rule(Y1, Y2),
78	remove_tautology_clauses(Y2, Y3),
79	abolish(input_clause, 1),
80	maplist(pred([C]:- assert(input_clause(C))), Y3).
81
82% main predicates.
83linear_prove(X, Y) :- linear_prove(X, Y, _, []).
84
85%
86linear_prove([], _, H, H):-!.
87linear_prove([X|R], Ance, [H|P], Q):- complementary(X, X1),
88	(	member(L, Ance),
89		copy_term(L, L0),
90		H = ancestor_resolution([X|R], L0)
91	;	input_clause(L0),
92		H = input_resolution([X|R], L0)
93	),
94	select(A, L0, L1),
95	unify_with_occurs_check(A, X1),
96	merge_clause_clause(L1, R, Y0),
97	sort(Y0, Y1),
98	has_no_complementary_pair(Y1),
99	copy_term(Y1, New),
101	linear_prove(Y1, Ance0, P, Q).
102%
103has_no_complementary_pair(X):- \+ has_complementary_pair(X).
104%
105has_complementary_pair([X|Y]):- has_complementary_pair(X, Y).
106has_complementary_pair([_|Y]):- has_complementary_pair(Y).
107%
108has_complementary_pair(X, [Y|_]):- complementary_pair(X, Y).
109has_complementary_pair(X, [_|Y]):- has_complementary_pair(X, Y).
110%
111complementary_pair(~A, B):- A==B.
112complementary_pair(A, ~B):- A==B.
113%
114add_to_ancestors(Y, [X|_], _):- subsumes_clause(Y, X), !, fail.
115add_to_ancestors(Y, [X|R], U):- subsumes_clause(X, Y), !,
119%
120complementary(~X, X):-!.
121complementary(X, ~X).
122%
123remove_tautology_clauses([X|Y], Y0):- has_complementary_pair(X), !,
124	remove_tautology_clauses(Y, Y0).
125remove_tautology_clauses([X|Y], [X|Y0]):- remove_tautology_clauses(Y, Y0).
126remove_tautology_clauses([], []).
127
128% ?- trace, fol:pure_literal_rule([[a,~b], [b, c(X)], [~c(Y), ~d], [~d]], R).
129%@ R = [[b, c(X)]].
130% ?- fol:pure_literal_rule([a/0, d/0], [[a,~b], [b, c(X)], [~c(Y), ~d], [~d]], R).
131%@ R = [[b, c(X)]].
132
133pure_literal_rule(X, Y):-  once(pure_literals_of_clauses(X, D)),
134	once(pure_literal_rule(D, X, Y)).
135%
136pure_literal_rule(D, [C|X], Y):-
137	(	member(A, C),
138		(	A = ~(A0),
139			functor(A0, F, N)
140		;	functor(A, F, N)
141		),
142		memberchk(F/N, D),
143		Y0 = Y
144	;	Y = [C|Y0]
145	),
146	!,
147	pure_literal_rule(D, X, Y0).
148pure_literal_rule(_, [], []).
149
150% ?- fol:pure_literals_of_clauses([[a, ~b, b, ~c(Y)]], R).
151%@ R = [a/0, c/1].
152pure_literals_of_clauses(X, Y):- literal_dict_list(X, [], R),
153	setof(F/N, Pos^Neg^C^(member(C, X),
154			      member([F, N, Pos, Neg], R),
155			      (var(Pos); var(Neg))),
156		Y),
157	!.
158pure_literals_of_clauses(_, []).
159
160		/*********************
161		*     subsumption    *
162		*********************/
163
164% ?- fol:merge_clause([a(f(A),B), a(B, A), a(C,C)], X).
165merge_cnf(X, Y):- once(merge_cnf_cnf(X, [], Y)).
166%
167merge_cnf_cnf([A|R], U, V):-
168	merge_cnf_clause(U, A, U0),
169	merge_cnf_cnf(R, U0, V).
170merge_cnf_cnf([], X, X).
171
172%
173merge_cnf_clause([A|R], C, S):-
174	(	subsumes_clause(C, A),
175		S = [A|R]
176	;	subsumes_clause(A, C),
177		merge_cnf_clause(R, C, S)
178	;	S = [A|S0],
179		merge_cnf_clause(R, C, S0)
180	).
181merge_cnf_clause([], C, [C]).
182
183%
184merge_clause(X, Y):- merge_clause_clause(X, [], Y).
185
186% ?- fol:merge_clause_clause([a,b,c], [a,b,d], X).
187merge_clause_clause([L|R], C,  S):-
188	merge_clause_literal(C, L, C0),
189	merge_clause_clause(R, C0, S).
190merge_clause_clause([], C, C).
191
192% ?- fol:merge_clause_literal([a(I,J),b,c],a(K,K), R).
193merge_clause_literal([A|R], C, S):-
194	(	subsumes_term(C, A),
195		S = [A|R]
196	;	subsumes_term(A, C),
197		merge_clause_literal(R, C, S)
198	;	S = [A|S0],
199		merge_clause_literal(R, C, S0)
200	).
201merge_clause_literal([], C, [C]).
202
203%  ?- fol:subsumes_clause([a,b], [a,b,c]).
204%  ?- fol:subsumes_clause([a,b,c], [a,b]).
205subsumes_clause(X, Y):- subsumes_clause_(Y, X).
206
207subsumes_clause_([X|R], C):- member(A, C),
208	subsumes_term(A, X),
209	!,
210	subsumes_clause_(R, C).
211subsumes_clause_([], _).
212
213% [2015/03/15]
214% ?- fol:negation_of_cnf([[a,b,c]], R), fol:negation_of_cnf(R, S).
215% ?- fol:negation_of_cnf([[a,b],[c,d]], R), fol:negation_of_cnf(R, S).
216% ?- fol:negation_of_cnf([[a,b],[c,d], [e,f]], R), fol:negation_of_cnf(R, S).
217negation_of_cnf(Cs, Neg):- 	choices(Cs, Ds0),
218	maplist(merge_clause, Ds0, Ds1),
219	maplist(maplist(complementary), Ds1, Ds),
220	merge_cnf(Ds, Neg).
221
222% ?- fol:literal_dict_list([[a,~b,b,c]], [], R).
223literal_dict_list([X|Y], D, D0):-
224	literal_dict(X, D, D1),
225	literal_dict_list(Y, D1, D0).
226literal_dict_list([], D, D).
227
228% ?- fol:literal_dict([a,~b,b,c], [], R).
229literal_dict([X|Y], D, D0):-
230	(	X = ~(A)
231	->	Neg = on
232	;	A = X,
233		Pos = on
234	),
235	functor(A, F, N),
236	(	memberchk([F, N, Pos, Neg],  D)
237	->	D1 = D
238	;	D1 = [[F, N, Pos, Neg]|D]
239	),
240	literal_dict(Y, D1, D0).
241literal_dict([], D, D).
242
243% ?- fol:set_of_support_proof([[a,~b], [a,b], [~a,b], [~a,~b]], [], 200, 5, S, Trace).
244% ?- fol:set_of_support_proof([[a,~b], [a,b], [~a,b], [~a,~b]], [[a,b]], 200, 5, S, Trace).
245% ?- fol:set_of_support_proof([[a,~b], [a,b], [~a,b], [~a,~b]], [[xxx]], 200, 5, S, Trace).
246set_of_support_proof(SOS, Centers, D, N, S, Trace):-
247	abolish(fol:input_clause, 1),
248	setup_input_clauses(SOS, X0),
249	X0 \== [],
250	maplist(pred([C]:- assert(input_clause(C))), X0),
251	(	Centers \== [], member(C0, Centers)
252	;	Centers  == [], input_clause(C0)
253	),
254	iterated_deepening( fol:linear_prove(C0, [], Trace, []),
255			   D, N, S).
256set_of_support_proof(_, _, _, _, fail, []).
257
258% ?- fol:number_to_var_name(6, X).
259number_to_var_name(I, X):- between(1, 6, I), memberchk(I-X, [1-x,2-y,3-z,4-u,5-v,6-w]).
260number_to_var_name(I, X):- I >= 7, J is I-6, atomic_concat(x, J, X).
261
262% for compatibility
263preprocess --> cnf, use_tilda_for_neg, remove_false, remove_true.
264
265use_tilda_for_neg --> maplist(maplist(not_to_tilda)).
266
267not_to_tilda(not(X), ~(X)):-!.
268not_to_tilda(X, X).
269
270remove_false --> maplist(variant(delete, false)).
271
272remove_true --> collect(fol:non_memberchk(true)).
273
274non_memberchk(X, Y):- \+ memberchk(X, Y).
275
276% cnf: convert to conjunctive normal form
277% ?- trace, fol:cnf(<-->(a,b), R).
278
279
280cnf --> internal,
281	macro,
282	prenex_normal_form,
283	math:boole_cnf,
284	math:simple_cnf.
285
286prenex_normal_form(X, Y):- fresh_bind(X, X0),
287	move_neg_inner(X0, X1),
288	skolemize(X1, Eqs),
289	maplist(ignore, Eqs),
290	forget_quantifier(X1, Y).
291
292%
293internal_form -->  internal, !, macro.
294
295
296% ?- fol:internal_form(<-->(a, <-->(b,c)), R).
297
298macro(imply(X,Y),or(not(A1),A2)):-!,macro(X,A1),macro(Y,A2) .
299macro(iff(X,Y),and(A1,A2)):-!,((macro(X,A3),macro(Y,A4)),macro(imply(A3,A4),A1)),(macro(Y,A5),macro(X,A6)),macro(imply(A5,A6),A2) .
300macro(X,Y):-(X=..[Q,V,F],fol:quantifier(Q)),!,macro(F,M),Y=..[Q,V,M] .
301macro(X,Y):-(X=..[F|X0],fol:logical_op(F)),!,maplist(macro,X0,Y0),Y=..[F|Y0] .
302macro(X,X):-! .
303
304forget_quantifier(every(A1,B),A2):-!,forget_quantifier(B,A2) .
305forget_quantifier(some(A1,B),A2):-!,forget_quantifier(B,A2) .
306forget_quantifier(and(X,Y),and(A1,A2)):-!,forget_quantifier(X,A1),forget_quantifier(Y,A2) .
307forget_quantifier(or(X,Y),or(A1,A2)):-!,forget_quantifier(X,A1),forget_quantifier(Y,A2) .
308forget_quantifier(X,X):-! .
309
310
311skolemize --> prenex, maplist(reverse), skolem_function.
312
313move_neg_inner --> inner_neg.
314
315
316inner_neg(not(not(X)),A1):-!,inner_neg(X,A1) .
317inner_neg(not(or(X,Y)),and(A1,A2)):-!,(inner_neg(X,A3),inner_neg(not(A3),A1)),inner_neg(Y,A4),inner_neg(not(A4),A2) .
318inner_neg(not(and(X,Y)),or(A1,A2)):-!,(inner_neg(X,A3),inner_neg(not(A3),A1)),inner_neg(Y,A4),inner_neg(not(A4),A2) .
319inner_neg(not(every(X,Y)),some(X,A1)):-!,inner_neg(Y,A2),inner_neg(not(A2),A1) .
320inner_neg(not(some(X,Y)),every(X,A1)):-!,inner_neg(Y,A2),inner_neg(not(A2),A1) .
321inner_neg(or(X,Y),or(A1,A2)):-!,inner_neg(X,A1),inner_neg(Y,A2) .
322inner_neg(and(X,Y),and(A1,A2)):-!,inner_neg(X,A1),inner_neg(Y,A2) .
323inner_neg(every(X,Y),every(X,A1)):-!,inner_neg(Y,A1) .
324inner_neg(some(X,Y),some(X,A1)):-!,inner_neg(Y,A1) .
325inner_neg(X,X):-! .
326
327
328% ?- fol:prenex(some(y, or(every(z, some(u, and(or(a(u,x), b(x)), every(v, c)))), d)), X).
329prenex(some(X, B), [[X]|P]):- prenex(B,  P).
330prenex(every(X, B), P):- prenex(B,  P0), maplist(cons(X), P0, P).
331prenex(and(X, Y), Z):- prenex(X, P), prenex(Y, Q), append(P, Q, Z).
332prenex(or(X, Y), Z):- prenex(X, P), prenex(Y, Q), append(P, Q, Z).
333prenex(_, []).
334
335skolem_function([], []):-!.
336skolem_function(Ps, Eqs):- length(Ps,N), numlist(1, N, Ns),
337	zip(Ns, Ps, Qs), maplist(skolem_function_, Qs, Eqs).
338
339zip([],[],[]).
340zip([A|B],[C|D],[(A,C)|R]):- zip(B, D, R).
341
342
343inverse(F, R, S):-setof(X, Y^(member(Y, R),member((X, Y), F)),S), !.
344inverse(_, _, []).
345
346skolem_function_((I, [Y|Xs]), Y= T):- atomic_list_concat(['\$sk', I],  F), T =.. [F|Xs].
347
348clausal_form(and(X), Y):-  !, maplist(drop_or, X, Y).
349clausal_form(or(X), [X]):- !.
350clausal_form(X, [[X]]).
351
352drop_or(or(L), L).
353drop_or(A, [A]).
354
355%%%%% example use of the prover fol.
356% ?- fol:prove_eq_leq(every(x,every(y, x=y -> same(x,y)))->every(x, same(x,x)), X).
357% X = valid.
358% ?- fol(every(x,every(y, x=y -> same(x,y)))->every(x, same(x,x)), X).
359% X = falsifiable.
360% ?- trace, fol(a, X).
361
362axiom_equiv((every(x, x=x),
363	     every(x, every(y, (x=y -> y=x))),
364	     every(x, every(y, every(z, (x=y, y=z) -> x=z))))).
365
366axiom_order((every(x, x=<x),
367	     every(x, every(y, (x=<y, y=<x) ->  x=y)),
368	     every(x, every(y, every(z, (x=<y, y=<z) -> x=<z))))).
369
370prove_eq_leq(X, Y):- axiom_equiv(A), axiom_order(B), fol((A,B) -> X, Y).
371
372%%%
373% ?- fol:external(every(X, some(Y, love(X,Y); love(Y,X))), A), print(A).
374
375default(C, D,  Cs, E):- member(M, Cs),
376	memberchk(C, M),
377	member(D, E),
378	memberchk(D, M).
379
380%%%
381connectives([ [(,), (&), and],
382	      [(;), or],
383	      [(\+), (~), not, -],
384	      [(->), imply],
385	      [(<-), inverse],
386	      [iff, (<->), (<=>), (<-->)],
387	      [every, all, forall],
388	      [some, exists] ]).
389
390logical_op(C) :- connectives(Cs), member(M, Cs), member(C, M).
391
392quantifiers([every, some, exists, forall, all]).
393
394quantifier(Q) :- quantifiers(Qs), member(Q, Qs).
395
396%
397internal_op([and, or, not, imply, inverse, iff, every, some]).
398
399internal_op(C, D):- connectives(Cs),
400	internal_op(E),
401	default(C, D, Cs, E).
402
403%
404external_op([(&), (;), (~), (->), (,), (-), <->, forall, some]).
405
406% ?- fol:external_op((or), X).
407external_op(C, D):- connectives(Cs),
408	external_op(E),
409	default(C, D, Cs, E).
410
411%%%%  rules to make an internal form
412
413% ?-  trace, fol:internal(some(x, a), R).
414% ?-  fol:internal((a,b), R).
415%@ R = (a, b) .
416% ?-  fol:internal(<-->(a,b), R), fol:macro(R, S).
417
418
419internal((X,Y),and(A1,A2)):-!,internal(X,A1),internal(Y,A2) .
420internal(X&Y,and(A1,A2)):-!,internal(X,A1),internal(Y,A2) .
421internal((X;Y),or(A1,A2)):-!,internal(X,A1),internal(Y,A2) .
422internal(~X,not(A1)):-!,internal(X,A1) .
423internal(-X,not(A1)):-!,internal(X,A1) .
424internal((X->Y),imply(A1,A2)):-!,internal(X,A1),internal(Y,A2) .
425internal((X-->Y),imply(A1,A2)):-!,internal(X,A1),internal(Y,A2) .
426internal(<-(X,Y),imply(A1,A2)):-!,internal(Y,A1),internal(X,A2) .
427internal(<--(X,Y),imply(A1,A2)):-!,internal(Y,A1),internal(X,A2) .
428internal(<->(X,Y),iff(A1,A2)):-!,internal(X,A1),internal(Y,A2) .
429internal(<-->(X,Y),iff(A1,A2)):-!,internal(X,A1),internal(Y,A2) .
430internal(X,Y):-(X=..[Q,V,F],quantifier(Q)),!,(internal_op(Q,Q0),internal(F,F0)),Y=..[Q0,V,F0] .
431internal(X,Y):-(X=..[F|X0],logical_op(F)),!,(internal(X0,A1),maplist(internal,A1,Y0)),Y=..[F|Y0] .
432internal(X,X):-! .
433
434
435% ?- listing(internal).
436% ?- fol:internal(<->(a,b), R), fol:external(R, E).
437% ?- fol:external(imply(a,imply(b,c)), R), fol:external(R, E).
438
439%%%%  Rule for making external form.
440
441external(X,Y):-(X=..[Q,V,F],quantifier(Q)),!,(external_op(Q,D),external(F,G)),Y=..[D,V,G] .
442external(X,Y):-(X=..[F|X0],logical_op(F)),!,(external_op(F,D),external(X0,A1),maplist(external,A1,Y0)),Y=..[D|Y0] .
443external(X,X):-!```