0

1 
LK: Classical FirstOrder Sequent Calculus


2 


3 
This directory contains the Standard ML sources of the Isabelle system for


4 
FirstOrder Logic as a classical sequent calculus. (For a Natural Deduction


5 
version, see FOL.) Important files include


6 


7 
ROOT.ML  loads all source files. Enter an ML image containing Pure


8 
Isabelle and type: use "ROOT.ML";


9 


10 
Makefile  compiles the files under Poly/ML or SML of New Jersey


11 


12 
ex  subdirectory containing examples. To execute them, enter an ML image


13 
containing LK and type: use "ex/ROOT.ML";


14 


15 


16 
Useful references on sequent calculi:


17 


18 
Jean Gallier, Logic for Computer Science (Harper&Row, 1986)


19 


20 
G. Takeuti, Proof Theory (North Holland, 1987)
