%% Version: 1.03p  -  Date: 08/04/01  -  File: leanCoP_o.pl
%%
%% Purpose: leanCoP: A Clausal Connection Prover for Classical Logic
%%
%% Author:  Jens Otten
%%
%% Usage:   prove(M,Proof).   % where M is a set of clauses
%%                            %  e.g. M=[[q(a)],[-p],[p, -q(X)]]
%%          prove(F,Proof).   % where F is a first-order formula
%%                            %  e.g. F=((p,all X:(p=>q(X)))=>all Y:q(Y))
%%                            %  (file nnfp_mm.pl is needed)

:- set_flag(occur_check,on).

%%% prove matrix M / formula F

prove([C|M],Proof) :- !, Time1 is cputime, prove([C|M],1,Proof),
                      Time2 is cputime, Time is Time2-Time1, print(Time).

prove(F,Proof) :- Time1 is cputime, make_matrix(F,M), prove(M,1,Proof),
                  Time2 is cputime, Time is Time2-Time1, print(Time).

prove(Mat,PathLim,[Cla|Proof]) :- %%
     append(MatA,[Cla|MatB],Mat), \+member(-_,Cla),
     append(MatA,MatB,Mat1),
     prove(Cla,[Cla|Mat1],[],PathLim,Proof). %%

prove(Mat,PathLim,Proof) :-
     nonground(Mat), PathLim1 is PathLim+1, prove(Mat,PathLim1,Proof).

prove([],_,_,_,[]).

prove([Lit|Cla],Mat,Path,PathLim,[[Cla2|Proof1]|Proof2]) :-
     (-NegLit=Lit;-Lit=NegLit) ->
        ( member(NegLit,Path), Cla2=[NegLit], Proof1=[]
          ;
          append(MatA,[Cla1|MatB],Mat), copy_term(Cla1,Cla2),
          append(ClaA,[NegLit|ClaB],Cla2), append(ClaA,ClaB,Cla3),
          ( Cla1==Cla2 ->
               append(MatB,MatA,Mat1)
               ;
               length(Path,K), K<PathLim,
               append(MatB,[Cla1|MatA],Mat1)
          ),
          prove(Cla3,Mat1,[Lit|Path],PathLim,Proof1)
        ),
        prove(Cla,Mat,Path,PathLim,Proof2).