%% Version:  1.08e  -  Date:  21/11/98  -  File: lintap.pl
%%
%% Purpose: linTAP: A Theorem Prover for Multiplicative Linear Logic M?LL
%%
%% Author:  Jens Otten
%% Web:     www.leancop.de/lintap/
%%
%% Usage:   prove(F).   % where F is a formula in M?LL (multiplicative
%%                      % linear logic with positive '?' and negative '!')
%%                      %  e.g. F=(((a@0)*a)@ ?(~a))
%%
%% Copyright: (c) 1998 by Jens Otten
%% License:   GNU General Public License


:- op(1110, xfy, @>).  :- op(1100, yfx, @).  :- op(1000, yfx, *).
:- op( 500,  fy, ~).   :- op( 500,  fy, !).  :- op( 500,  fy, ?).


%%% Prove formula F

prove(F):- A is cputime, pp(F,0), B is cputime, C is B-A, print(C).

pp(F,I) :- display(I), nl, 
           prove([(F,0),[0],l],[],[],0,I,PU,At,Bt,[],C1),
           length(Bt,Nbt), length(C1,Nc1), Nc1=:=(2*Nbt)+2,
           length(At,Nat), Nc1=:=Nat+Nbt+1,
           t_string_unify(PU).
pp(F,I) :- I1 is (I+1), pp(F,I1).


%%% Specification of Tableau Rules for M?LL

fml(A,   Pol, S,[A,Pol],[],      [],[S],0):-var(A).
fml((A@B), 0, S, (A,0), [],   (B,0),[S],0).
fml((A*B), 1, S, (A,1), [],   (B,1),[S],0).
fml((A@>B),0, S, (A,1), [],   (B,0),[S],0).
fml((A@B), 1, _, (A,1), (B,1),[],[_],0).
fml((A*B), 0, _, (A,0), (B,0),[],[_],0).
fml((A@>B),1, _, (A,0), (B,1),[],[_],0).
fml((!A),  1, S, (A,1), [],((!A),1),[S],c).
fml((!A),  1, _, (A,1), [],   [], [],0).
fml((?A),  0, S, (A,0), [],((?A),0),[S],c).
fml((?A),  0, _, (A,0), [],   [], [],0).
fml(0,     1, S, (S,0), [],   (S,1),[S],0).
fml(1,     0, S, (S,0), [],   (S,1),[S],0).
fml(1,     1, _, (X,0), (X,1),[],[_],0).
fml(0,     0, _, (X,0), (X,1),[],[_],0).
fml((~A),  0, _, (A,1), [],      [], [],0).
fml((~A),  1, _, (A,0), [],      [], [],0).
fml(A,   Pol, S,[A,Pol],[],   [],[S],0).


%%% Path Checking

prove([(F,Pol),Pre,P],UnExp,Lits,Exp,ExpLim,PU,At,Bt,C,C1) :-
   fml(F,Pol,P,F1,F2,F3,PrN,Cpy), append(_,[Lp],Pre),
   ( Cpy=c -> Exp<ExpLim, Exp1 is (Exp+1) ; Exp1=Exp, ! ),
   ( (F2\=[],var(Lp);F2=[],\+var(Lp)) -> Pre1=Pre;append(Pre,PrN,Pre1) ),

   (F3=[] ->  F1a=F1,F3a=F3 ; F3=(G3,_),F1=(G1,_),
    ( \+var(G1),F3\=[],(F1=(?_,0);F1=(!_,1)) -> (F1a=F3,F3a=[];F1a=F1,F3a=F3) ;
      \+var(G1),F3\=[],F1=(X,X) -> F1a=F3,F3a=[] ;
      \+var(G3),Cpy\=c,(F3=(?_,0);F3=(!_,1)) -> F1a=F1,(F3a=[];F3a=F3) ;
      \+var(G3),F3=(X,X) -> F1a=F1,F3a=[] ; F1a=F1, F3a=F3 )),

   ( F3a=[] -> UnExp1=UnExp, At=At3;
              UnExp1=[[F3a,Pre1,r(P)]|UnExp], At=[P|At3] ),
   prove([F1a,Pre1,l(P)],UnExp1,Lits,Exp1,ExpLim,PU1,At1,Bt1,C,C2),
   ( F2=[] -> PU=PU1, At3=At1, Bt=Bt1, C1=C2 ;
     prove([F2,Pre1,r(P)],UnExp1,Lits,Exp1,ExpLim,PU2,At2,Bt2,C2,C1),
     append(PU1,PU2,PU), union(At1,At2,At3), union([P|Bt1],Bt2,Bt) ).

prove([[Lit,Pl],Pr,P],_,[[[L,Pl1],Pr1,P1]|Lits],_,_,PU,At,Bt,C,C1) :-
   ( Lit=L, Pl is 1-Pl1, Lit=L,  At=[], Bt=[],
     (member([P,S],C)  -> (S=P1 -> C1=C, PU=[]) ;
     (member([P1,S],C) -> (S=P  -> C1=C, PU=[]) ;
      PU=[[Pr,_]=[Pr1,_]], C1=[[P,P1],[P1,P]|C])) ) ;
   prove([[Lit,Pl],Pr,P],[],Lits,_,_,PU,At,Bt,C,C1).
prove(Lit,[Next|UnExp],Lits,Exp,ExpLim,PU,At,Bt,C,C1) :-
   prove(Next,UnExp,[Lit|Lits],Exp,ExpLim,PU,At,Bt,C,C1).


%%% T-String Unification

t_string_unify([]).
t_string_unify([S=T|G]):- flatten(S,S1,[]), flatten(T,T1,[]),
                          tunify(S1,[],T1), t_string_unify(G).
tunify([],[],[]).
tunify([X1|S],[],[X2|T])      :- X1==X2, !, tunify(S,[],T).
tunify([V|S],Z,[])            :- V=Z, tunify(S,[],[]).
tunify([V,X|S],[],[V1|T])     :- var(V1), tunify([V1|T],[V],[X|S]).
tunify([V,X|S],[Z1|Z],[V1|T]) :- var(V1), append([Z1|Z],[Vnew],V),
                                 tunify([V1|T],[Vnew],[X|S]).
tunify([V|S],Z,[X|T])         :- (S=[]; T\=[]; \+var(X)) ->
                                 append(Z,[X],Z1), tunify([V|S],Z1,T).

flatten(A,[A|B],B) :- (var(A); A\=[], A\=[_|_]), !.
flatten([],A,A).
flatten([A|B],C,D) :- flatten(A,C,E), flatten(B,E,D).