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),
  100	once(add_to_ancestors(New, Ance, Ance0)),
  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), !,
  116	add_to_ancestors(Y, R, U).
  117add_to_ancestors(Y, [X|R], [X|U]):- add_to_ancestors(Y, R, U).
  118add_to_ancestors(Y, [], [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):-!