%% Version: 1.00  -  Date: 18/03/01  -  File: proof_leancop.pl
%%
%% Purpose: Presentation of Connection Proof found by leanCoP
%%
%% Author:  Jens Otten
%%
%% Usage:   proof_leancop(M,P).  % where M is a matrix and P is the
%%                               % connection proof found by leanCoP
%%                               %  e.g. M=[[q(a)],[-p],[p, -q(X)]]
%%                               %       P=[[q(a)],[[p,-(q(a))],
%%                               %         [[-(p)]]]]


proof_leancop(Mat,Proof) :-
     print_compact_proof(Proof), nl,
     display('======================================================'), nl,
     print_connect_proof(Mat,Proof), nl,
     display('======================================================'), nl,
     print_long_proof(Mat,Proof), nl,
     display('======================================================'), nl.


%%% print compact proof

print_compact_proof(Proof) :-
     %% Proof=[[[-(!)|Ctail]|Ptail]], Proof1=[Ctail|Ptail],
     nl, display('Compact Proof:'), nl,
     display('--------------'), nl,
     print_term(Proof), nl.


%%% print connection proof

print_connect_proof(Mat,Proof) :-
     %% Proof=[[[-(!)|Ctail]|Ptail]], Proof1=[Ctail|Ptail],
     nl, display('Proof for the following Clauses:'), nl,
     print_clauses(Mat,1),
     display('Connection Proof:'), nl,
     display('-----------------'), nl,
     print_proof(Mat,Proof,[]).

print_proof(Mat,[Cla|Tail],I) :-
     print_step(I), display('  '), print_term(Cla),
     clause_number(Cla,Mat,1,Num),
     display('   ('), display(Num), display(')'), nl,
     print_proof2(Mat,Tail,[1|I]).

print_proof2(_,[],_).
print_proof2(Mat,[Cla|Tail],I) :-
     print_proof(Mat,Cla,I), I=[J1|J], J2 is J1+1, I1=[J2|J],
     print_proof2(Mat,Tail,I1).


%%% print long proof

print_long_proof(Mat,Proof) :-
     %% Proof=[[[-(!)|Ctail]|Ptail]], Proof1=[Ctail|Ptail],
     nl, display('Proof for the following Clauses:'), nl,
     print_clauses(Mat,1),
     display('Long Proof:'), nl,
     display('-----------'), nl,
     print_intro,
     print_lproof(Mat,Proof,[],[],[]),
     print_end.

print_lproof(Mat,[Cla|Tail],I,Lit,Path) :-
     print_step(I), display('  '), clause_number(Cla,Mat,1,Num),
     ( Lit=[] ->
          Cla1=Cla
          ;
          display('Assume '), print_term(Lit), display(' is true. '),
          (-NegLit=Lit;-Lit=NegLit) -> delete(NegLit,Cla,Cla1),
          display('Then '), print_term(NegLit), display(' is false.'),
          nl, print_sp(I), display('  ')
     ),
     ( Num=reduction ->
          display('This is a contradiction to assumption '),
          clause_number(NegLit,Path,1,NumP),
          append(Ih,It,I), length(Ih,NumP),
          print_step(It), display('.'), nl
	  ;
          Cla1=[] ->
               display('Then clause ('), display(Num), display(') '),
               display('is false.'), nl
	       ;
               display('Clause ('), display(Num), display(') '),
               display('is true if at least one of the following '),
               display('statements is true:'),
               nl, print_sp(I), display('  '), print_term(Cla1), nl,
               print_sp(I), print_subs(Cla,Mat),nl
      ),
      print_lproof2(Mat,Tail,[1|I],Cla1,[Lit|Path]).

print_lproof2(_,[],_,_,_).
print_lproof2(Mat,[Cla|Tail],I,[Lit|Scl],Path) :-
     print_lproof(Mat,Cla,I,Lit,Path),
     I=[J1|J], J2 is J1+1, I1=[J2|J],
     print_lproof2(Mat,Tail,I1,Scl,Path).


%%% print

print_term(Term) :- print(Term).

print_step([]).
print_step([I])     :- display(I).
print_step([I,J|T]) :- print_step([J|T]), display('.'), display(I).

print_sp([]).
print_sp([I]) :- I<1.
print_sp([I]) :- I>=1, display(' '), I1 is I/10, print_sp([I1]).
print_sp([I,J|T]) :- print_sp([J|T]), display(' '), print_sp([I]).

print_intro :- 
     display('To prove:'), nl,
     display('The given clauses are inconsistent, i.e. for every'), nl,
     display('interpretation of the predicates the clauses evaluate'), nl,
     display('to "false". The proof is by contradiction: Assume that'), nl,
     display('the given clauses are consistent, i.e. there is some'), nl,
     display('interpretation, so that the clauses evaluate to "true".'), nl,
     display('Then there has to be at least one statement in each'), nl,
     display('clause which is true.'), nl, nl.

print_end :- nl,
    display('Therefore there is no interpretation which makes all'), nl,
    display('given clauses simultaneously true. Hence the given'), nl,
    display('clauses are inconsistent.'), nl,
    display('                                              q.e.d.'), nl.

print_clauses([],_) :- nl.
print_clauses([Cla|Mat],I) :-
     display(' ('), display(I), display(')  '), print_term(Cla), nl,
     I1 is I+1, print_clauses(Mat,I1).

%%% misc

clause_number(_,[],_,'reduction').
clause_number(Cla,[Cla1|Mat],I,I1) :-
     \+ \+ Cla=Cla1 -> I1=I ; I2 is I+1, clause_number(Cla,Mat,I2,I1).

print_subs(Cla,[Cla1|Mat]) :-
     \+ Cla=Cla1 -> print_subs(Cla,Mat) ;
     term_variables(Cla1,L), display('  Variables '), print_term(L),
     Cla=Cla1, display(' are substituted by '), print_term(L),
     print_term(' .'), fail.
print_subs(_,_).