src/FOL/README.html
changeset 1331 70ee8d7b2233
child 3279 815ef5848324
equal deleted inserted replaced
1330:e9becade0076 1331:70ee8d7b2233
       
     1 <HTML><HEAD><TITLE>FOL/ReadMe</TITLE></HEAD><BODY>
       
     2 
       
     3 <H2>FOL: First-Order Logic with Natural Deduction</H2>
       
     4 
       
     5 This directory contains the Standard ML sources of the Isabelle system for
       
     6 First-Order Logic (constructive and classical versions).  For a classical
       
     7 sequent calculus, see LK.  Important files include
       
     8 
       
     9 <DL>
       
    10 <DT>ROOT.ML
       
    11 <DD>loads all source files.  Enter an ML image containing Pure
       
    12 Isabelle and type: use "ROOT.ML";<P>
       
    13 
       
    14 <DT>Makefile
       
    15 <DD>compiles the files under Poly/ML or SML of New Jersey<P>
       
    16 
       
    17 <DT>ex
       
    18 <DD>subdirectory containing examples.  To execute them, enter an ML image
       
    19 containing FOL and type: use "ex/ROOT.ML";<P>
       
    20 </DL>
       
    21 
       
    22 Useful references on First-Order Logic:
       
    23 
       
    24 <UL>
       
    25 <LI>Antony Galton, Logic for Information Technology (Wiley, 1990)
       
    26 <LI>Michael Dummett, Elements of Intuitionism (Oxford, 1977)
       
    27 </UL>
       
    28 </BODY></HTML>