% paramodulation-0.1.elf
% First-order paramodulation
% Author: Carsten Schuermann

%%%%%%%%%%%%%%%%%%%%%%%%%%
% Terms
%%%%%%%%%%%%%%%%%%%%%%%%%%

i    : type.

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

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

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


#  : o -> o -> type.			%infix  right 10 #.
|- : o -> type.			%prefix 9 |-.
refl    : |- T == T.
trans   : |- S == T -> |- T == U -> |- S == U.
symm    : |- S == T -> |- T == S.
paramod : {P} (S == T) # C -> (P S) # D -> |- or C (or D (P T)).
select  : |- A -> A # false.
inst    : |- (all A)  -> |- (A X).
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.