%% prove(F).   % where F is a first-order formula, e.g.:
%%
%% prove(all X: (m(X) & ~m(X))).
%% prove(ex X: (m(X) v ~m(X))).
%% prove(~(all X: (p(X)) => (ex Y:p(Y)))).
%% prove( ~(ex X:( all Y:p(X,Y)) => ex X: (ex Y:p(X,Y)))).
%% prove( ~(ex X:p(X) & (all Y:r(Y)) <=>  ex X:(ex Y:(p(X) & r(Y))))).
%% prove( ~(((ex X:p(X)) & (all Y:r(Y))) <=> ( ex W:(all Z:(p(W) & r(Z)))))).
%%
%% Nav realizets: 
%%       -- funkciju konstantes, 
%%       -- atrasta modela/interpretacijas paradisana konsistentam formulam,
%%       -- eksistences kvantori tiek apstradati ar skolemizaciju (nevis ta ka nodarbiba stastija)
%%       -- operatoru prioritates varetu nebut isti pareizas, tapec vajag drosi lietot iekavas,
%%          it seviski pie kvantoriem, lai pareizi noraditu to scope (iekavas nekad neskade)
%%
%% Programmas butiskas dalas nemtas no Beckert&Posegga "leanTAP", tikai izlabotas dazas drukas
%% kludas, sis tas vienkarsots vai pielikts klat lai rezultatu druka skaidra cilveku valoda.

:- op(1130, xfy, <=>). % equivalence
:- op(1110, xfy, =>).  % implication
:- op(1000, xfy, v).   % disjunction
:- op(1000, xfy, &).   % conjunction
:- op( 500, fy, ~).    % negation
:- op( 500, fy, all).  % universal quantifier
:- op( 500, fy, ex).   % existential quantifier
:- op( 500,xfy, :).

prove(Fml) :- nnf(Fml,NNF), write('Skolemized NNF:  '), writeln(NNF), 
      (prove(NNF,[],[],[],100),!, writeln('Formula is proved inconsistent (VarLim < 100)');
       writeln('The full-width search did not prduce result within VarLim=100.'),
       writeln('Continuing possibly infinite depth-first search which can miss inconsistency; increase VarLim to force full-width search up to VarLim)...'),
        writeln('(Ctrl/C to terminate)'),
       \+prove(NNF,[],[],[],_),!, writeln(''), writeln('Formula is proved consistent in finite time');
       prove(NNF,[],[],[],_),!, writeln('Formula is proved inconsistent (VarLim > 100)')).


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

prove((A v B),UnExp,Lits,FreeV,VarLim) :- !,prove(A,UnExp,Lits,FreeV,VarLim),
                                          prove(B,UnExp,Lits,FreeV,VarLim). % Disjunction

prove(all(X:Fml),UnExp,Lits,FreeV,VarLim) :- !, (not(not(VarLim=anything)),!;\+length(FreeV,VarLim)), 
    copy_term((X,Fml,FreeV),(X1,Fml1,FreeV)), append(UnExp,[all(X:Fml)],UnExp1),
    prove(Fml1,UnExp1,Lits,[X1|FreeV],VarLim). %Universal Quantification

prove(Lit,_,[L|Lits],_,_) :- (Lit = ~Neg; ~Lit = Neg) -> 
    ( unify_with_occurs_check(Neg,L); prove(Lit,[],Lits,_,_)). % Closing Branches

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


nnf(Fml,NNF) :- nnf(Fml,[],NNF).

nnf(Fml,FreeV,NNF) :- 
	(Fml = ~(~A)      -> Fml1 = A;
	 Fml = ~(all X:F) -> Fml1 = (ex X: ~F);
	 Fml = ~(ex X:F)  -> Fml1 = (all X: ~F);
	 Fml = ~((A v B)) -> Fml1 = ((~A & ~B));
	 Fml = ~((A & B)) -> Fml1 = (~A v ~B);
	 Fml = (A => B)   -> Fml1 = (~A v B);
	 Fml = ~((A => B))-> Fml1 = ((A & ~B));
	 Fml = (A <=> B)  -> Fml1 = ((A & B) v (~A & ~B));
	 Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) v (~A & B)) ),!,
	nnf(Fml1,FreeV,NNF).

nnf((all X:Fml),FreeV,all(X:NNF)) :- !,  
	nnf(Fml,[X|FreeV],NNF).

nnf((ex X:Fml),FreeV,NNF) :- !,  %% Skolemization
	copy_term((X,Fml,FreeV),(Fml,Fml1,FreeV)),  
	nnf(Fml1,FreeV,NNF).

nnf((A & B),FreeV,(NNF1 & NNF2)) :- !,  
	nnf(A,FreeV,NNF1), nnf(B,FreeV,NNF2).

nnf((A v B),FreeV,(NNF1 v NNF2)) :- !, 
	nnf(A,FreeV,NNF1), nnf(B,FreeV,NNF2).

nnf(Lit,_,Lit).