%Define a predicate $sko\_fun(X,Y)$, whre $X$ is a list of free variables, and $Y$ is a previously unused Skolem function symbol applied to those free variables.

/* below solution is old-fashioned and for explanatory purposes only; an alternative would be to use the gensym library */

:- assert(m:funcount(1)).

newfuncount(N) :-
   m:funcount(N),
   retract(m:funcount(N)),
   M is N+1,
   assert(m:funcount(M)).

/*   reset :- the Skolem function index is reset to 1.
*/

reset :-
   retract(m:funcount(_)),
   assert(m:funcount(1)),
   !.

sko_fun(Varlist, Skoterm) :-
   newfuncount(N),
   Skoterm =.. [fun | [N | Varlist]].

%Extend the propositional tableau prover (Solutions 4) to a first-order theorem
%prover.

/* operator definition */

:-op(140,fy,[~,?,!,neg]).
:-op(160, yfx, [&, and, or]).
:-op(160, xfy, :).
:-op(180, yfx, '!=').
:-op(200, xfy, [imp, =>]).
:-op(200, xfy, [bimp, <=>]).
:-op(400,xfx,\).

/* type definitions */

is_unary(neg neg _X).
is_unary(neg true).
is_unary(neg false).

is_binary(X) :- member(X,[and, or, imp]).

is_conjunctive(_X and _Y).
is_conjunctive(neg(_X or _Y)).
is_conjunctive(neg(_X imp _Y)).
is_conjunctive(_X bimp _Y).

is_disjunctive(neg(_X and _Y)).
is_disjunctive(_X or _Y).
is_disjunctive(_X imp _Y).
is_disjunctive(neg(_X bimp _Y)).

is_universal(all(_,_)).
is_universal(neg some(_,_)).

is_existential(some(_,_)).
is_existential(neg all(_,_)).

is_literal(X) :-
	\+ is_conjunctive(X),
	\+ is_disjunctive(X),
	\+ is_unary(X),
	\+ is_universal(X),
	\+ is_existential(X).

is_atomicfmla(X) :-
	is_literal(X),
	X \= neg _.

component(neg neg X, X).
component(neg true, false).
component(neg false, true).

components(X and Y, X,Y).
components(neg(X and Y), neg X, neg Y).
components(X or Y,X,Y).
components(neg(X or Y), neg X, neg Y).
components(X imp Y, neg X, Y).
components(neg(X imp Y), X, neg Y).
components(X bimp Y, neg X or Y, neg Y or X).
components(neg(X bimp Y), X and neg Y, Y and neg X).

/*   notation(Notated, Free) :-
         Notated is a notated formula, and Free is its
         associated free variable list.
*/

notation(n(X, _Y), X).

/*   fmla(Notated, Formula) :-
         Notated is a notated formula, and Formula is its
         formula part.
*/

fmla(n(_X, Y), Y).

/*   singlestep(OldTableau, OldQdepth,
            NewTableau, NewQdepth) :-
         the application of one tableau rule to OldTableau,
         with a Q-depth of OldQdepth, will produce the
         tableau NewTableau, and will change the available
         Q-depth to NewQdepth.
*/

remove(_X,[],[]).
remove(X,[X|Xs],Ys) :-
	remove(X,Xs,Ys).
remove(X,[Y|Xs],[Y|Ys]) :-
	X \== Y,
	remove(X,Xs,Ys).

/*   sub(Term, Variable, Formula, NewFormula) :-
         NewFormula is the result of substituting
         occurrences of Term for each free
         occurrence of Variable in Formula.
*/

sub(Term, Variable, Formula, NewFormula) :-
	sub1(Term, Variable, Formula, NewFormula) , !.

sub1(Term, Var, A, Term) :- Var == A.
sub1(_Term, _Var, A, A) :- atomic(A).
sub1(_Term, _Var, A, A) :- var(A).

sub1(Term, Var, neg X, neg Y) :-
	sub1(Term, Var, X, Y).

sub1(Term, Var, Binary_One, Binary_Two) :-
	is_binary(F),
	Binary_One =.. [F, X, Y],
	Binary_Two =.. [F, U, V],
	sub1(Term, Var, X, U),
	sub1(Term, Var, Y, V).

sub1(_Term, Var, all(Var, Y), all(Var, Y)).
sub1(Term, Var, all(X, Y), all(X, Z)) :-
	sub1(Term, Var, Y, Z).
sub1(_Term, Var, some(Var, Y), some(Var, Y)).
sub1(Term, Var, some(X, Y), some(X, Z)) :-
	sub1(Term, Var, Y, Z).

sub1(Term, Var, Functor, Newfunctor) :- 
	Functor =.. [F | Arglist],
	sub_list(Term, Var, Arglist, Newarglist),
	Newfunctor =.. [F | Newarglist].

sub_list(Term, Var, [Head | Tail], [Newhead | Newtail]) :-
	sub1(Term, Var, Head, Newhead),
	sub_list(Term, Var, Tail, Newtail).

sub_list(_Term, _Var, [], []).

/*  instance(F, Term, Ins) :-
         F is a quantified formula, and Ins is the result
         of removing the quantifier and replacing all
         free occurrences of the quantified variable by
         occurrences of Term.
*/

instance(all(X,Y), Term, Z) :- sub(Term, X, Y, Z).
instance(neg some(X,Y), Term, neg Z) :- sub(Term, X, Y, Z).
instance(some(X,Y), Term, Z) :- sub(Term, X, Y, Z).
instance(neg all(X,Y), Term, neg Z) :- sub(Term, X, Y, Z).

/* Fitting's free variable tableau prover */

singlestep([OldBranch | Rest], Qdepth,
      [NewBranch | Rest], Qdepth) :-
   member(NotatedFormula, OldBranch),
   notation(NotatedFormula, Free),
   fmla(NotatedFormula, Formula),
   is_unary(Formula),
   component(Formula, NewFormula),
   notation(NewNotatedFormula, Free),
   fmla(NewNotatedFormula, NewFormula),
   remove(NotatedFormula, OldBranch, TempBranch),
   NewBranch = [NewNotatedFormula | TempBranch].

singlestep([OldBranch | Rest], Qdepth,
      [NewBranch | Rest], Qdepth) :-
   member(NotatedAlpha, OldBranch),
   notation(NotatedAlpha, Free),
   fmla(NotatedAlpha, Alpha),
   is_conjunctive(Alpha),
   components(Alpha, AlphaOne, AlphaTwo),
   notation(NotatedAlphaOne, Free),
   fmla(NotatedAlphaOne, AlphaOne),
   notation(NotatedAlphaTwo, Free),
   fmla(NotatedAlphaTwo, AlphaTwo),
   remove(NotatedAlpha, OldBranch, TempBranch),
   NewBranch =
     [NotatedAlphaOne, NotatedAlphaTwo | TempBranch].

singlestep([OldBranch | Rest], Qdepth,
      [NewBranchOne, NewBranchTwo | Rest], Qdepth) :-
   member(NotatedBeta, OldBranch),
   notation(NotatedBeta, Free),
   fmla(NotatedBeta, Beta),
   is_disjunctive(Beta),
   components(Beta, BetaOne, BetaTwo),
   notation(NotatedBetaOne, Free),
   fmla(NotatedBetaOne, BetaOne),
   notation(NotatedBetaTwo, Free),
   fmla(NotatedBetaTwo, BetaTwo),
   remove(NotatedBeta, OldBranch, TempBranch),
   NewBranchOne = [NotatedBetaOne | TempBranch],
   NewBranchTwo = [NotatedBetaTwo | TempBranch].

singlestep([OldBranch | Rest], Qdepth,
      [NewBranch | Rest], Qdepth) :-
   member(NotatedDelta, OldBranch),
   notation(NotatedDelta, Free),
   fmla(NotatedDelta, Delta),
   is_existential(Delta),
   sko_fun(Free, Term),
   instance(Delta, Term, DeltaInstance),
   notation(NotatedDeltaInstance, Free),
   fmla(NotatedDeltaInstance, DeltaInstance),
   remove(NotatedDelta, OldBranch, TempBranch),
   NewBranch = [NotatedDeltaInstance | TempBranch].

singlestep([OldBranch | Rest], OldQdepth,
      NewTree, NewQdepth) :-
   member(NotatedGamma, OldBranch),
   notation(NotatedGamma, Free),
   fmla(NotatedGamma, Gamma),
   is_universal(Gamma),
   OldQdepth > 0,
   remove(NotatedGamma, OldBranch, TempBranch),
   NewFree = [V | Free],
   instance(Gamma, V, GammaInstance),
   notation(NotatedGammaInstance, NewFree),
   fmla(NotatedGammaInstance, GammaInstance),
   append([NotatedGammaInstance | TempBranch], 
     [NotatedGamma], NewBranch),
   append(Rest, [NewBranch], NewTree),
   NewQdepth is OldQdepth-1.

singlestep([Branch | OldRest], OldQdepth,
      [Branch | NewRest], NewQdepth) :-
   singlestep(OldRest, OldQdepth, NewRest, NewQdepth).


/*   expand(Tree, Qdepth, Newtree) :-
         the complete expansion of the tableau Tree,
         allowing Qdepth applications of the gamma
         rule, is Newtree.
*/

expand(Tree, Qdepth, Newtree) :-
   singlestep(Tree, Qdepth, TempTree, TempQdepth),
   expand(TempTree, TempQdepth, Newtree).
expand(Tree, _Qdepth, Tree).


/*   closed(Tableau) :- every branch of Tableau can be
        made to contain a contradiction, after a suitable
        free variable substitution.
*/

closed([Branch | Rest]) :-
   member(Falsehood, Branch),
   fmla(Falsehood, false),
   closed(Rest).

closed([Branch | Rest]) :-
   member(NotatedOne, Branch),
   fmla(NotatedOne, X),
   is_atomicfmla(X),
   member(NotatedTwo, Branch),
   fmla(NotatedTwo, neg Y),
   unify_with_occurs_check(X, Y),
   closed(Rest).

closed([ ]).

/*   if_then_else(P, Q, R) :-
         either P and Q, or not P and R.
*/

if_then_else(P, Q, _R) :- P, !, Q.
if_then_else(_P, _Q, R) :- R.

/*   valid(X, Qdepth) :- create a complete tableau expansion
        for neg X, allowing Qdepth applications of the
        gamma rule.  Test for closure.
*/

valid(X, Qdepth) :- 
   reset,
   notation(NotatedFormula, [ ]),
   fmla(NotatedFormula, neg X),
   expand([[NotatedFormula]], Qdepth, Tree),
   if_then_else(closed(Tree), yes(Qdepth), no(Qdepth)).

/*   unsat(X, Qdepth) :- create a complete tableau expansion
        for X, allowing Qdepth applications of the
        gamma rule.  Test for closure.
*/

unsat(X, Qdepth) :- 
   reset,
   notation(NotatedFormula, [ ]),
   fmla(NotatedFormula, X),
   expand([[NotatedFormula]], Qdepth, Tree),
   if_then_else(closed(Tree), yes(Qdepth), no(Qdepth)).

yes(Qdepth) :-
   write('First-order tableau theorem at Q-depth '),
   write(Qdepth),
   write(.),
   nl.

no(Qdepth) :-
   write('Not a first-order tableau theorem at Q-depth '),
   write(Qdepth),
   write('.'),
   nl.

%:- valid(some(w,all(x,r(x,w,f(x,w)))) imp some(w,all(x,some(y,r(x,w,y)))),5).
%:- valid(some(w,all(x,r(x,w,f(x,w)))) imp some(w,all(x,some(y,r(x,w,y)))),0).
%:- valid(some(x,all(y,r(x,y))) imp all(y,some(x,r(x,y))),5).
%:- valid(all(x,some(y,r(x,y))) imp some(y,all(x,r(x,y))),5).
%:- valid(some(x,p(x) imp all(x,p(x))),5).
%:- valid(some(x,(p(x) or q(x))) imp (some(x,p(x)) or some(x,q(x))),5).
%:- valid(some(x,(p(x) and q(x)) imp (some(x,p(x)) and some(x,q(x)))),5).
%:- valid((some(x,p(x)) and some(x,q(x))) imp some(x,(p(x) and q(x))),5).
%:- valid(all(x,(p(x) or q(x))) imp (some(x,p(x)) or (all(x,q(x)))),2).
%:- unsat(neg (all(x,(p(x) or q(x))) imp (some(x,p(x)) or (all(x,q(x))))),2).
%:- valid(((a or b) and (a or c) and (a or d) and (a or e) and (b or c) and (c or d) and (d or e)) or neg (((a or b) and (a or c) and (a or d) and (a or e) and (b or c) and (c or d) and e)),0).