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
   83% ?- add_new_variant(a, [], X).
   84% ?- add_new_variant(a, [b,c], X).
   85% ?- add_new_variant(a, [b,c,a], X).
   86
   87add_new_variant(X, [], [X]):-!.
   88add_new_variant(X, [Y|Ys], R):-
   89	(	variant(X, Y) -> fail
   90	; 	R = [Y|Zs],
   91		add_new_variant(X, Ys, 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),
  164		add_new_variant(Zs, History, History0),
  165		solve(Zs, Bs, CNF, History0, J, M, R)
  166	)