% -----------------------------------------------------------------
% leancop_pure.pl - A connection prover implemented in Prolog
% -----------------------------------------------------------------

:- [nnf_mm].
:- [unify].

% -----------------------------------------------------------------
prove(M) :- M=[_|_] -> prove(M,1) ;
                       make_matrix(M,M1), prove(M1,1).

prove(M,I) :- print(iteration:I), nl,
              member(C1,M), copy_term(C1,C2),
              prove(C2,M,[],I).
prove(M,I) :- I1 is I+1, prove(M,I1).
% -----------------------------------------------------------------

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

% reduction
prove([L1|C],M,Path,I) :- (L1= -N1; -L1=N1) ->
                          member(L2,Path), unify1(N1,L2),
                          prove(C,M,Path,I).
% extension
prove([L1|C],M,Path,I) :- \+ length(Path,I),
                          (L1= -N1; -L1=N1) ->
                          member(C1,M), copy_term(C1,C2),
                          select1(L2,C2,C3), unify1(N1,L2),
                          prove(C3,M,[L1|Path],I),
                          prove(C,M,Path,I).

% -----------------------------------------------------------------
select1(X,L,L1) :- append(L2,[X|L3],L), append(L2,L3,L1).
% -----------------------------------------------------------------