%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% An Implementation of G4ip for Terzo
% 	author: Christian.Urban@cl.cam.ac.uk 
% 
% some solvable sample queries:
%
% prove (nil |- p imp p).
% prove (nil |- (p imp p) imp (p imp p)).
% prove (nil |- ((((p imp q) imp p) imp p) imp q) imp q).
% prove (nil |- (a imp (b imp c)) imp ((a imp b) imp (a imp c))).
% prove (nil |- (a or (a imp b)) imp (((a imp b) imp a) imp a)).
%
% two non-solvable queries
%
% prove (nil |- a or (a imp false)).
% prove (nil |- ((a imp b) imp a) imp a).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

module G4ip.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% atomic formulae
kind form type.

type p form. 
type q form.
type a form.
type b form.
type c form.

type isatomic form -> o.

isatomic p.
isatomic q.
isatomic a.
isatomic b.
isatomic c.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% logical operators
type false  form.
type and    form -> form -> form.    
type or     form -> form -> form.       
type imp    form -> form -> form.
 
infixr and   9.
infixr or    9.
infixr imp   9.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% sequent constructor; sequents are of the form: (list |- formula) 
kind seq type.

type   |-  list form -> form -> seq. 
infixl |-   4.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% prove predicate; prints "solvable" if seq is provable, otherwise "no" 
type prove seq -> o.

prove (Gamma |- G) :- ( membNrest P Gamma Gamma',
                        left (P::Gamma' |- G) );
                        right   (Gamma  |- G).   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% rightrules
type right seq -> o.

right (Gamma |- B and C) :- prove (Gamma |- B),          %% and-R   
                            prove (Gamma |- C).          

right (Gamma |- B imp C) :- prove (B::Gamma |- C).       %% imp-R

right (Gamma |- B or  C) :- prove (Gamma |- B);          %% or-R 
                            prove (Gamma |- C).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% leftrules
type left  seq -> o.

left (false :: Gamma |- G).                              %% false-L

left (A :: Gamma |- A)     :- isatomic A.                %% axiom 

left (B and C::Gamma |- G) :- prove (B::C::Gamma |- G).  %% and-L
 
left (B  or C::Gamma |- G) :- prove (B::Gamma |- G),     %% or-L 
                              prove (C::Gamma |- G).


left (A imp B::Gamma |- G) :-                            %% imp-L1
	isatomic A, ismember A Gamma, prove (B::Gamma |- G).

left ((B and C) imp D::Gamma |- G) :-                    %% imp-L2
	prove (B imp (C imp D)::Gamma |- G).

left ((B or  C) imp D::Gamma |- G) :-                    %% imp-L3
	prove (B imp D::C imp D::Gamma |- G).

left ((B imp C) imp D::Gamma |- G) :-                    %% imp-L4
	prove (C imp D::Gamma |- B imp C),	                              
	prove (D::Gamma |- G).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% returns a member and the remainder of a list
type membNrest     A -> list A -> list A -> o.

membNrest X (X::Rest) Rest.
membNrest X (Y::Tail) (Y::Rest) :- membNrest X Tail Rest.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% succeeds only once if A is element in the list 
type ismember     A -> list A -> o.

ismember X (X::Rest) :- !.
ismember X (Y::Tail) :- ismember X Tail.