28:- use_module(library(lists)).  % load module for lists
   29:- use_module(library(terms)).  % load module for terms
   30:- [def_mm].  % load program for clausal form translation
   31:- dynamic(pathlim/0). :- dynamic(lit/4).   32
   33
   34%%% prove matrix M / formula F
   35
   36prove(F,Proof) :- prove2(F,[cut,comp(7)],Proof).
   37
   38prove2(F,Set,Proof) :-
   39    (F=[_|_] -> M=F ; make_matrix(F,M,Set)),
   40    retractall(lit(_,_,_,_)), (member([-(#)],M) -> S=conj ; S=pos),
   41    assert_clauses(M,S), prove(1,Set,Proof).
   42
   43prove(PathLim,Set,Proof) :-
   44    \+member(scut,Set) -> prove([-(#)],[],PathLim,[],Set,[Proof]) ;
   45    lit(#,_,C,_) -> prove(C,[-(#)],PathLim,[],Set,Proof1),
   46    Proof=[C|Proof1].
   47prove(PathLim,Set,Proof) :-
   48    member(comp(Limit),Set), PathLim=Limit -> prove(1,[],Proof) ;
   49    (member(comp(_),Set);retract(pathlim)) ->
   50    PathLim1 is PathLim+1, prove(PathLim1,Set,Proof).
   51
   52%%% leanCoP core prover
   53
   54prove([],_,_,_,_,[]).
   55
   56prove([Lit|Cla],Path,PathLim,Lem,Set,Proof) :-
   57    Proof=[[[NegLit|Cla1]|Proof1]|Proof2],
   58    \+ (member(LitC,[Lit|Cla]), member(LitP,Path), LitC==LitP),
   59    (-NegLit=Lit;-Lit=NegLit) ->
   60       ( member(LitL,Lem), Lit==LitL, Cla1=[], Proof1=[]
   61         ;
   62         member(NegL,Path), unify_with_occurs_check(NegL,NegLit),
   63         Cla1=[], Proof1=[]
   64         ;
   65         lit(NegLit,NegL,Cla1,Grnd1),
   66         unify_with_occurs_check(NegL,NegLit),
   67         ( Grnd1=g -> true ; length(Path,K), K<PathLim -> true ;
   68           \+ pathlim -> assert(pathlim), fail ),
   69         prove(Cla1,[Lit|Path],PathLim,Lem,Set,Proof1)
   70       ),
   71       ( member(cut,Set) -> ! ; true ),
   72       prove(Cla,Path,PathLim,[Lit|Lem],Set,Proof2).
   73
   74%%% write clauses into Prolog's database
   75
   76assert_clauses([],_).
   77assert_clauses([C|M],Set) :-
   78    (Set\=conj, \+member(-_,C) -> C1=[#|C] ; C1=C),
   79    (ground(C) -> G=g ; G=n), assert_clauses2(C1,[],G),
   80    assert_clauses(M,Set).
   81
   82assert_clauses2([],_,_).
   83assert_clauses2([L|C],C1,G) :-
   84    assert_renvar([L],[L2]), append(C1,C,C2), append(C1,[L],C3),
   85    assert(lit(L2,L,C2,G)), assert_clauses2(C,C3,G).
   86
   87assert_renvar([],[]).
   88assert_renvar([F|FunL],[F1|FunL1]) :-
   89    ( var(F) -> true ; F=..[Fu|Arg], assert_renvar(Arg,Arg1),
   90      F1=..[Fu|Arg1] ), assert_renvar(FunL,FunL1)