% -----------------------------------------------------------------
% leantap_pure.pl - A tableau prover implemented in Prolog
% -----------------------------------------------------------------

:- [nnf_pure].
:- [unify].

% -----------------------------------------------------------------
prove(F) :- nnf(F,F1), prove(F1,1).

prove(F,I) :- print(iteration:I), nl,
              prove(F,[],[],[],I).
prove(F,I) :- I1 is I+1, prove(F,I1).
% -----------------------------------------------------------------

% alpha rule
prove((A|B),UnExp,Lits,FreeV,VarLim) :- !,
	prove(A,[B|UnExp],Lits,FreeV,VarLim).

% beta rule
prove((A&B),UnExp,Lits,FreeV,VarLim) :- !,
	prove(A,UnExp,Lits,FreeV,VarLim),
	prove(B,UnExp,Lits,FreeV,VarLim).
        
% gamma rule
prove((?[X]:Fml),UnExp,Lits,FreeV,VarLim) :- !,
	\+ length(FreeV,VarLim),
	copy_term((X,Fml,FreeV),(X1,Fml1,FreeV)),
	append(UnExp,[(?[X]:Fml)],UnExp1),
	prove(Fml1,UnExp1,Lits,[X1|FreeV],VarLim).

% axiom
prove(Lit,_,Lits,_,_) :-
	(Lit = ~Neg; ~Lit = Neg) ->
	member(L,Lits), unify1(Neg,L).

% next
prove(Lit,[Next|UnExp],Lits,FreeV,VarLim) :-
	prove(Next,UnExp,[Lit|Lits],FreeV,VarLim).

% -----------------------------------------------------------------