/* Gentzen's LK for Propositional Logic */


:- op(800,xfx,'#-').

predicates([ #- ]).




X+Y=Y+X.
X+(Y+Z)=(X+Y)+Z.


H+i(A) #- G+i(A).					% axiom

H #- i(and(A,B))+G <-  H #- i(A)+G, H #- i(B)+G.	% and right

i(and(A,B))+H #- G <-  i(A)+i(B)+H #- G.		% and left

H #- i(or(A,B))+G  <-  H #- i(A)+i(B)+G.		% or right

i(or(A,B))+H #- G  <-  i(A)+H #- G, i(B)+H #- G.	% or left


H #- i(imp(A,B))+G <-  i(A)+H #- i(B)+G.		% impl right

i(imp(A,B))+H #- G <-  H #- i(A)+G, i(B)+H #- G.	% imp left

H #- i(not(A))+G   <-  i(A)+H #- G.			% not right

i(not(A))+H #- G   <-  H #- i(A)+G.			% not left





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:-option([ac(on),crw_depth(2)]).

precedence([+,'#-',i,not,and,or,imp,1,0]). 


% Linear polynomial interpretations for AC-operators
% must have the form X+Y+c, otherwise they won't be
% AC-compatible. Nonlinear interpretations for AC-symbols f(X,Y)
% must be of the form aXY+b(X+Y)+c where ac+b-b^2=0.

% Warning: at this point nothing is checked about admissibility
%          and competeness of polynomial interpretations.
%          Right now, polynomials have to be linear and
%          an interpretation must be provided for any symbol
%          in the signature.
%          Works only under SICStus 3


:-ordering(poly([

	(X+Y)      	- (X+Y), 
	(A #- B)   	- (A+B), 
	and(A,B)   	- (2*A+2*B),
	or(A,B)    	- (2*A+2*B),
	imp(A,B)   	- (16*A+4*B),
	not(A)     	- 4*A,
	i(A)       	- 2*A,
	1 		- 2, 
	0 		- 2]),

    		
	poly).	



:-sama([]).
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).

/*

In the given polynomial interpretation, ``prove'' atoms have (only)
exponentially many smaller atoms, hence provability in this
sequent calculus is in DEXPTIME.


In this version of LK we try to avoid problems that arise from
the fact that one should consider the ``right +''
and ``left +'' as having units 0 and 1. 
Hence, ground sequents are assumed to have the form

        i(A1)+ ... +i(Ak)+1 #- i(B1)+ ... +i(Bn)+0


with end markers 0 and 1, respectively, k,n>=0,
and Ai and Bi boolean expressions formed from variables
and the logical symbols not, and, or and imp.



With the ordering given above, in all clauses the head atom
is strictly maximal, hence the system is trivially saturated.



Saturation terminated.

Persisting Clauses:

    1(1) : B+C=C+B
    2(1) : B+(C+D)=B+C+D
    3(1) : B+i(C)#-D+i(C)
    4(1) : B#-i(C)+D,B#-i(E)+D -> B#-i(and(C,E))+D
    5(1) : i(B)+i(C)+D#-E -> i(and(B,C))+D#-E
    6(1) : B#-i(C)+i(D)+E -> B#-i(or(C,D))+E
    7(1) : i(B)+C#-D,i(E)+C#-D -> i(or(B,E))+C#-D
    8(1) : i(B)+C#-i(D)+E -> C#-i(imp(B,D))+E
    9(1) : B#-i(C)+D,i(E)+B#-D -> i(imp(C,E))+B#-D
   10(1) : i(B)+C#-D -> C#-i(not(B))+D
   11(1) : B#-i(C)+D -> i(not(C))+B#-D



Total time: 1330 milliseconds

*/