1:- module(fol_prover, []).    2
    3:- use_module(util('fol-cnf')).    4:- use_module(zdd(zdd)).    5:- use_module(zdd('zdd-array')).    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:- op(200, fy, ~).   12:- op(400, yfx, &).   13
   14:- nb_setval(prove_time_limit, 60).   15
   16% ?- prove(all(x, all(y, p)) -> p).
   17% ?- prove(all(X, p(X))-> some(Y, (p(Y), p(f(Y))))).
   18% ?- prove(all(X, p(X))-> some(Y, (p(Y), -p(f(Y))))).
   19% ?- prove((all(Y, p(Y))-> some(X, (p(X),  -p(f(X)))))).
   20% ?- prove((all(Y, p(Y))-> -some(X, (p(X),  -p(f(X)))))).
   21
   22		/*********************
   23		*     Resolution     *
   24		*********************/
   25
   26% ?- BarberSentence =
   27%	(all(x, barber(x) ==  all(y,  -shave(y, y) == shave(x, y)))),
   28%	time(prove(( BarberSentence -> -some(x, (barber(x), shave(x, x)))))).
   29% ?- Barber =
   30%	(all(x, barber(x) ==  all(y,  -shave(y, y) == shave(x, y)))),
   31%	DontShave = all(x, (barber(x)-> -shave(x,x))),
   32%	time(prove((Barber -> DontShave))).
   33
   34set_when_gt(I, J, S):-
   35	(	I =< J -> true
   36	;	nb_setarg(1, S, 1)
   37	).
   38%
   39apply_options([], X, X).
   40apply_options([P|Ps], X, Y):- call(P, X, Z),
   41	apply_options(Ps, Z, Y).
   42
   43		/***********************
   44		*     Linear Solver    *
   45		***********************/
   46
   47% ?- prove(a->a).
   48% ?- prove(-(a->a)).
   49% ?- prove(a;a).
   50% ?- prove(a).
   51
   52prove(P):- prove(P, Out), writeln(Out).
   53
   54%
   55prove(P, Out):-
   56	fol_cnf(-P, Cs),
   57	fol_cnf(P, Ds),
   58	nb_getval(prove_time_limit, T),
   59	call_with_time_limit(T, dual_solve(Cs, Ds, 2, R, U)),
   60	( nonvar(R) -> Out =  R
   61	; Out = U
   62	).
   63
   64% ?- solve_with_iterated_deepening([[a],[-a]], 2).
   65% ?- solve_with_iterated_deepening([[a, -b],[a], [b]], 2).  % false.
   66%
   67solve_with_iterated_deepening(Cs, K):-
   68	with_depth_limit_solve(Cs, K, Success, Exceed),
   69	(	nonvar(Success)	-> true
   70	;	arg(1, Exceed, 0) -> fail
   71	;   K0 is 2*K,
   72		solve_with_iterated_deepening(Cs, K0)
   73	).
   74
   75dual_solve(Cs, NegCs, K, R, U):-
   76	with_depth_limit_solve(Cs, K, Success_a, Exceed_a),
   77	with_depth_limit_solve(NegCs, K, Success_b, Exceed_b),
   78	(	nonvar(Success_a) -> R = valid
   79	;	nonvar(Success_b) -> R = unsatisfiable
   80	;	arg(1, Exceed_a, 0) -> U = invalid
   81	;	arg(1, Exceed_b, 0) -> U = weakly_satisfiable %   but unknown validity
   82	;	K0 is 2*K,
   83		dual_solve(Cs, NegCs, K0, R, U)
   84	).
   85%
   86with_depth_limit_solve(Cs, K, Success, Exceed):-
   87	Exceed = $(0),
   88	(	member(C, Cs),
   89		solve_center(Cs, [C], [], 0, K, Success, Exceed),
   90		nonvar(Success) -> true
   91	;	true
   92	).
   93
   94%
   95solve_center(_, [], _, _, _, 'SOLVED', _):-!.
   96solve_center(Cs, [[]|C], A, J, K, Success, Exceed):-!,
   97	J > 0,
   98	J0 is J - 1,
   99	solve_center(Cs, C, A, J0, K, Success, Exceed).
  100solve_center(Cs, [[X|Y]|C], A, J, K, Success, Exceed):- ancestor_check(X, A), !,
  101	(	Y = [] ->  solve_center(Cs, C, A, J, K, Success, Exceed)
  102	;	solve_center(Cs, [Y|C], A, J, K, Success, Exceed)
  103	).
  104solve_center(_, _, _,  J, K, _, Exceed):- J > K, !, nb_setarg(1, Exceed, 1).
  105solve_center(Cs, [[X|Y]|C], A, J, K, Success, Exceed):-
  106	flip_polarity(X, X0),
  107	resolvent(X0, Cs, G),
  108	add_variant(X, A, A0),
  109	J0 is J + 1,
  110	(	Y = [] ->
  111		solve_center(Cs, [G|C], A0, J0, K, Success, Exceed)
  112	;	solve_center(Cs, [G, Y|C], A0, J0, K, Success, Exceed)
  113	).
  114
  115% ?- add_variant(a(X), [a(Y)], R).
  116% ?- add_variant(a(X), [b(Y)], R).
  117add_variant(X, Y, Y0):-
  118	(	member(M, Y), variant(X, M) ->
  119		Y0 = Y
  120	;	copy_term(X, X0),
  121		Y0 = [X0|Y]
  122	).
  123
  124% ?- ancestor_check(a(X), [a(Y)]).
  125% ?- ancestor_check(a(X), [b(Y)]).
  126ancestor_check(X, Y):-member(M, Y), variant(X, M).
  127
  128% ?- resolvent(a, [[a],[b]], R).
  129% ?- resolvent(a, [[b],[a,c]], R).
  130% ?- resolvent(a(X, 1), [[a(2, Y)]], R).
  131resolvent(X, E, R):-
  132	member(M, E),
  133	copy_term(M, M0),
  134	select(Y, M0, R),
  135	unify_with_occurs_check(X, Y).
  136
  137% ?- unify_complementary_literals(-a, a).
  138% ?- unify_complementary_literals(-a(X, 1), a(2, Y)).
  139% ?- unify_complementary_literals(-a(X, 1), -b(2, Y)).
  140% unify_complementary_literals(X, Y):-
  141% 	flip_polarity(X, X0),
  142% 	unify_with_occurs_check(X0, Y).
  143
  144% set-of-support as given centers plus input (but without exact definition.)
  145% ?- set_of_support(a, a).
  146% ?- set_of_support((a->b)*a, b).
  147set_of_support(P, Cen):- set_of_support(P, Cen, 30).
  148%
  149set_of_support(P, Cen, Tlimit):- fol_cnf(P, E),
  150	fol_cnf(-Cen, Cen0),
  151	Cen0 \== [],
  152	call_with_time_limit(Tlimit, solve_center(E, Cen0, 2)).
  153
  154% ?- solve_center([[a, -b]],[[a], [b]], 2).
  155solve_center(E, Cen, K):- Ex = $(0),
  156	member(C, Cen),
  157	linear_solve(E, [C], [], 0, K, R, Ex),
  158	(	nonvar(R)-> true
  159	;	arg(1, Ex, 0) -> fail
  160	;   K0 is 2*K,
  161		solve_center(E, Cen, K0)
  162	).
  163%
  164set_of_support_clausal(P, Cen):- set_of_support_clausal(P, Cen, 30).
  165%
  166set_of_support_clausal(P, Cen, Tlimit):- cgi:rename_vars(P, E),
  167	cgi:rename_vars(Cen, Cen0),
  168	call_with_time_limit(Tlimit, solve_center_clause(E, Cen0, 2)).
  169
  170% ?- solve_center_clause([[a, -b]],[[a], [b]], 2).
  171solve_center_clause(E, [], K):-!, solve_with_iterated_deepening(E, K).
  172solve_center_clause(E, Cen, K):- Ex = $(0),
  173	member(C, Cen),
  174	solve_with_iterated_deepening(E, [C], [], 0, K, R, Ex),
  175	(	nonvar(R)-> true
  176	;	arg(1, Ex, 0) -> fail
  177	;   K0 is 2*K,
  178		solve_center_clause(E, Cen, K0)
  179	).
  180
  181		/******************************************
  182		*     pure literal law, unit law, etc.    *
  183		******************************************/
  184
  185% ?-pure_literal_law([[a]], X).
  186% ?-pure_literal_law([[a],[b]], X).
  187% ?-pure_literal_law([[a(X), -b(X)],[b(Y), -a(Y)]], X).
  188% ?-pure_literal_law([[a(X), b(X)],[a(Y), b(Y)]], R).
  189% ?-pure_literal_law([[a(X)]], R).
  190
  191pure_literal_law(Cs, Ds):- 	pure_literal_signs(Cs, Ps),
  192	pure_literal_law(Cs, Ds, Ps).
  193%
  194pure_literal_law([], [], _):-!.
  195pure_literal_law([C|Cs], Ds, Ps):-
  196	member(X, C),
  197	ltr_check(X, _, _, P),
  198	memberchk(P, Ps),
  199	!,
  200	pure_literal_law(Cs, Ds, Ps).
  201pure_literal_law([C|Cs], [C|Ds], Ps):-	pure_literal_law(Cs, Ds, Ps).
  202
  203% ?- pure_literal_signs([[a(X), b(X)], [c, d]], Ps).
  204% ?- pure_literal_signs([[a, b], [-a, d]], Ps).
  205pure_literal_signs(Cs, Ps):-
  206	positive_literal_signs(Cs, P),
  207	sort(P, P0),
  208	negative_literal_signs(Cs, N),
  209	sort(N, N0),
  210	subtract(P0, N0, A),
  211	subtract(N0, P0, B),
  212	union(A, B, Ps).
  213
  214% ?- positive_literal_signs([[a, a], [-b, -c]], P).
  215positive_literal_signs(Cs, Ps):-
  216	findall(P,
  217			(	member(C, Cs),
  218				member(L, C),
  219				ltr_check(L, +, _, P)
  220			),
  221			Ps0
  222		   ),
  223	sort(Ps0, Ps).
  224
  225% ?- negative_literal_signs([[a], [-b, -c]], P).
  226negative_literal_signs(Cs, Ps):-
  227	findall(P,
  228			(	member(C, Cs),
  229				member(L, C),
  230				ltr_check(L, -, _, P)
  231			),
  232			Ps0
  233		   ),
  234	sort(Ps0, Ps)