?-op(140,fy,neg).
?-op(160, xfx, [and, or, imp, revimp, nand, nor, notimp, notrevimp]).

member(X,[X|_]).
member(X,[_|Xs]) :- member(X,Xs).

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

append([],Xs,Xs).
append([X|Xs],Ys,[X|Zs]) :-
	append(Xs,Ys,Zs).

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

is_binary(X) :-
	member(X,[and, or, imp, revimp, nand, nor, notimp, notrevimp]).

is_conjunctive(_X and _Y).
is_conjunctive(neg(_X or _Y)).
is_conjunctive(neg(_X imp _Y)).
is_conjunctive(neg(_X revimp _Y)).
is_conjunctive(neg(_X nand _Y)).
is_conjunctive(_X nor _Y).
is_conjunctive(_X notimp _Y).
is_conjunctive(_X notrevimp _Y).

is_disjunctive(neg(_X and _Y)).
is_disjunctive(_X or _Y).
is_disjunctive(_X imp _Y).
is_disjunctive(_X revimp _Y).
is_disjunctive(_X nand _Y).
is_disjunctive(neg(_X nor _Y)).
is_disjunctive(neg(_X notimp _Y)).
is_disjunctive(neg(_X notrevimp _Y)).

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 revimp Y, X, neg Y).
components(neg(X revimp Y), neg X, Y).
components(X nand Y, neg X, neg Y).
components(neg (X nand Y), X,Y).
components(X nor Y,neg X, neg Y).
components(neg(X nor Y), X,Y).
components(X notimp Y, X, neg Y).
components(neg(X notimp Y), neg X, Y).
components(X notrevimp Y, neg X, Y).
components(neg(X notrevimp Y), X, neg Y).

% this comes directly from Fitting
%
% todo (17.01.2006): improve and remove non-declarative features

/*  unify(Term1, Term2) :-
       Term1 and Term2 are unified with the occurs check.
       See Sterling and Shapiro, The Art of Prolog.
*/

unify(X,Y) :-
     var(X), var(Y), X=Y.
unify(X,Y) :-
     var(X), nonvar(Y), not_occurs_in(X,Y), X=Y.
unify(X,Y) :-
     var(Y), nonvar(X), not_occurs_in(Y,X), Y=X.
unify(X,Y) :-
     nonvar(X), nonvar(Y), atomic(X), atomic(Y), X=Y.
unify(X,Y) :-
     nonvar(X), nonvar(Y),
     compound(X), compound(Y),
     term_unify(X,Y).

not_occurs_in(X,Y) :-
     var(Y),
     X \== Y.
not_occurs_in(_X,Y) :-
     nonvar(Y),
     atomic(Y).
not_occurs_in(X,Y) :-
     nonvar(Y),
     compound(Y),
     functor(Y,_F,N),
     not_occurs_in(N,X,Y).

not_occurs_in(N,X,Y) :-
     N>0, arg(N,Y,Arg), not_occurs_in(X,Arg), N1 is N-1,
     not_occurs_in(N1,X,Y).
not_occurs_in(0,_X,_Y) .

term_unify(X,Y) :-
     functor(X,F,N), functor(Y,F,N), unify_args(N,X,Y).

unify_args(N,X,Y) :-
     N>0, unify_arg(N,X,Y), N1 is N-1, unify_args(N1,X,Y).
unify_args(0,_X,_Y).

unify_arg(N,X,Y) :-
     arg(N,X,ArgX), arg(N,Y,ArgY), unify(ArgX,ArgY).

% compound(X) :- functor(X,_,N), N>0.
% built-in predicate of sicstus

/*   universal(X) :- X is a gamma formula.
*/

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

/*   existential(X) :- X is a delta formula.
*/

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

/*   literal(X) :- X is a literal.
*/
% todo (17.01.2006): very ugly, improve as fast as possible
%

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

/*   atomicfmla(X) :- X is an atomic formula.
*/

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

/*   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).


/*   newfuncount(N) :-
         N is the current Skolem function index, and as a
         side effect, the remembered value is incremented.
*/

% assert as user does not work, hence the module m
%

:- 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(X, Y) :-
         X is a list of free variables, and Y is a
         previously unused Skolem function symbol
         applied to those free variables.
*/

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

/*   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.
*/

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(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.

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

test(X, Qdepth) :- 
   reset,
   notation(NotatedFormula, [ ]),
   fmla(NotatedFormula, neg 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.

% I want to see the tableau proof
%

gen_tableau(X,Qdepth,Tree) :-
	reset,
	notation(NotatedFormula, []),
	fmla(NotatedFormula, neg X),
	expand([[NotatedFormula]], Qdepth, Tree).

gen_notated_fms([],[]).
gen_notated_fms([X|Xs],[NX|NXs]) :-
	notation(NX,[]),
	fmla(NX, neg X),
	gen_notated_fms(Xs,NXs).

gen_tableau2(Xs,Qdepth,Tree) :-
	reset,
	gen_notated_fms(Xs,NXs),
	expand([NXs], Qdepth, Tree).
% tests
:- test(some(w,all(x,r(x,w,f(x,w)))) imp some(w,all(x,some(y,r(x,w,y)))),5).
:- test(some(w,all(x,r(x,w,f(x,w)))) imp some(w,all(x,some(y,r(x,w,y)))),0).
:- test(some(x,all(y,r(x,y))) imp all(y,some(x,r(x,y))),5).
:- test(all(x,some(y,r(x,y))) imp some(y,all(x,r(x,y))),5).
:- test(some(x,p(x) imp all(x,p(x))),5).
:- test(some(x,(p(x) or q(x)) imp (some(x,p(x)) or some(x,q(x)))),5).
:- test(some(x,(p(x) and q(x)) imp (some(x,p(x)) and some(x,q(x)))),5).
:- test((some(x,p(x)) and some(x,q(x))) imp some(x,(p(x) and q(x))),5).
:- test(all(x,(p(x) or q(x))) imp (some(x,p(x)) or (all(x,q(x)))),2).
:- gen_tableau2([all(x,p(x) or q(x)),all(x,neg p(x)),some(x,neg q(x))],1,Xs).