0

1 
FOL: FirstOrder Logic with Natural Deduction


2 


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


4 
FirstOrder Logic (constructive and classical versions). For a classical


5 
sequent calculus, see LK. 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 FOL and type: use "ex/ROOT.ML";


14 


15 
Useful references on FirstOrder Logic:


16 


17 
Antony Galton, Logic for Information Technology (Wiley, 1990)


18 


19 
Michael Dummett, Elements of Intuitionism (Oxford, 1977) 