% resolution-1.0.elf
% Propositional resultion
% Author: Carsten Schuermann

%%%%%%%%%%%%%%%%%%%%%%%%%%
% Formulas
%%%%%%%%%%%%%%%%%%%%%%%%%%

o    : type.
neg   : o -> o.
or    : o -> o -> o.
false : o.
=>    : o -> o -> o 
      = [A][B] or (neg A) B.		%infix right 11 =>.


%%%%%%%%%%%%%%%%%%%%%%%%%%
% Derivability
%%%%%%%%%%%%%%%%%%%%%%%%%%


#  :  o -> o -> type.			%infix  right 10 #.
|- :  o -> type.			%prefix 9 |-.
resolve : A # B -> (neg A) # C -> |- or B C.
select  : |- A -> A # false.
left    : (or A B) # C -> A # (or B C).
right   : (or A B) # C -> B # (or A C).
id1     : |- or false A -> |- A.
id2     : |- or A false -> |- A.
id3     : |- A -> |- or A false.
id4     : |- A -> |- or false A.