:-op(140,fy,neg).
:-op(160,xfx,[and, or, imp]).
:-op(400,xfx,\).

select_first(X,[X|Xs],Xs).
select_first(X,[Y|Ys],[Y|Zs]) :-
	X \=Y,
	select_first(X,Ys,Zs).

append_dl(Xs\Ys,Ys\Zs,Xs\Zs).

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_disjunctive(neg(_X and _Y)).
is_disjunctive(_X or _Y).
is_disjunctive(_X imp _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).

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

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

/*   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) :-
	gensym(skofun,SkolemFS),
	Skoterm =.. [SkolemFS | 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(Bs1\Bs,Qdepth,NBs1\NBs,NQdepth) :-
	nonvar(Bs1),
	singlestep2(Bs1\Bs,Qdepth,NBs1\NBs,NQdepth).

singlestep2([OldBranch|Rest1] \ Rest, Qdepth,[NewBranch|Rest1] \ Rest, Qdepth) :-
	member(NotatedFormula, OldBranch),
	notation(NotatedFormula, Free),
	fmla(NotatedFormula, Formula),
	is_unary(Formula),
	component(Formula, NewFormula),
	notation(NewNotatedFormula, Free),
	fmla(NewNotatedFormula, NewFormula),
	select_first(NotatedFormula, OldBranch, TempBranch),
	append([NewNotatedFormula], TempBranch, NewBranch).
singlestep2([OldBranch | Rest1] \ Rest, Qdepth,[NewBranch | Rest1] \ 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),
	select_first(NotatedAlpha, OldBranch, TempBranch),
	append([NotatedAlphaOne, NotatedAlphaTwo], TempBranch, NewBranch).
singlestep2([OldBranch | Rest1] \ Rest, Qdepth, [NewBranchOne, NewBranchTwo | Rest1] \ 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),
	select_first(NotatedBeta, OldBranch, TempBranch),
	append([NotatedBetaOne], TempBranch, NewBranchOne),
	append([NotatedBetaTwo], TempBranch, NewBranchTwo).
singlestep2([OldBranch | Rest1] \ Rest, Qdepth,[NewBranch | Rest1] \ 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),
	select_first(NotatedDelta, OldBranch, TempBranch),
	append([NotatedDeltaInstance],TempBranch,NewBranch).
singlestep2([OldBranch | Rest1] \ Rest, OldQdepth,NewTree, NewQdepth) :-
	member(NotatedGamma, OldBranch),
	notation(NotatedGamma, Free),
	fmla(NotatedGamma, Gamma),
	is_universal(Gamma),
	OldQdepth > 0,
	select_first(NotatedGamma, OldBranch, TempBranch),
	NewFree = [V | Free],
	instance(Gamma, V, GammaInstance),
	notation(NotatedGammaInstance, NewFree),
	fmla(NotatedGammaInstance, GammaInstance),   
	append([NotatedGammaInstance | TempBranch] , [NotatedGamma], NewBranch),
	append_dl(Rest1 \ Rest, [NewBranch|Xs]\Xs, NewTree),
	NewQdepth is OldQdepth-1.
singlestep2([Branch | OldRest1] \ OldRest, OldQdepth,[Branch | NewRest1] \NewRest, NewQdepth) :-
	singlestep(OldRest1\OldRest, OldQdepth, NewRest1\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(Bs1\Bs) :-
	var(Bs1),
	Bs1 == Bs.
closed(Bs1 \ Bs) :-
	nonvar(Bs1),
	Bs1 = [Branch|Bs2],
	member(Falsehood, Branch),
	fmla(Falsehood, false),
	closed(Bs2 \ Bs).
closed(Bs1\ Bs) :-
	nonvar(Bs1),
	Bs1 = [Branch|Bs2],
	member(NotatedOne, Branch),
	fmla(NotatedOne, X),
	is_atomicfmla(X),
	member(NotatedTwo, Branch),
	fmla(NotatedTwo, neg Y),
	unify_with_occurs_check(X, Y),
	closed(Bs2 \ Bs).


/*   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_gensym(skofun),
	notation(NotatedFormula, [ ]),
	fmla(NotatedFormula, neg (X)),
	expand([[NotatedFormula]|Ts]\Ts, 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,FrmTree) :-
	reset_gensym(skofun),
	notation(NotatedFormula, []),
	fmla(NotatedFormula, neg (X)),
	gen_tableau2([[NotatedFormula]|Ts]\Ts, Qdepth, Tree),
	projection(Tree,FrmTree).

gen_tableau2(Tree,_Qdepth,Tree1) :-
	Tree = Tree1\[].
gen_tableau2(OldTree,Qdepth0,NewTree) :-
	singlestep(OldTree, Qdepth0, NewTree0, Qdepth1),
	gen_tableau2(NewTree0,Qdepth1,NewTree).

projection([],[]).
projection([Branch|Tree],[FrmBranch|FrmTree]) :-
	projection_branch(Branch,FrmBranch),
	projection(Tree,FrmTree).

projection_branch([],[]).
projection_branch([NotatedFormula|Bs],[Formula|FBs]) :-
	fmla(NotatedFormula,Formula),
	projection_branch(Bs,FBs).


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

% lecture
:- test(all(x,(p(x) or q(x))) imp (some(x,p(x)) or (all(x,q(x)))),2).
:- test(some(x,all(y,r(x,y))) imp all(y,some(x,r(x,y))),5).
:- test(some(w,all(x,r(x,w,f(x,w)))) imp some(w,all(x,some(y,r(x,w,y)))),5).
:- test(all(x,all(y,(p(x) and p(y)))) imp all(x,all(y,(p(x) or p(y)))),2).
:- test(all(x,some(y,all(z,some(w,r(x,y) or neg r(w,z))))),4).