src/Sequents/README.html
author paulson
Wed Oct 09 13:32:33 1996 +0200 (1996-10-09)
changeset 2073 fb0655539d05
child 3279 815ef5848324
permissions -rw-r--r--
New unified treatment of sequent calculi by Sara Kalvala
combines the old LK and Modal with the new ILL (Int. Linear Logic)
     1 <!-- $Id$ -->
     2 <HTML><HEAD><TITLE>Sequents/ReadMe</TITLE></HEAD><BODY>
     3 
     4 <H2>Sequents: Various Sequent Calculi</H2>
     5 
     6 This directory contains the Standard ML sources of the Isabelle system for
     7 various Sequent, Linear, and Modal Logic.  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";
    13 
    14 <DT>Makefile
    15 <DD>compiles the files under Poly/ML or SML of New Jersey
    16 
    17 
    18 <DT>ex
    19 <DD>subdirectory containing examples.  Files are arranged in
    20 subdirectories. To execute all of them, enter an ML image containing
    21 Sequents and type 
    22 <PRE>
    23 	use "ex/ROOT.ML";
    24 </PRE>
    25 To execute examples in a particular logic (LK/ILL/Modal) use the
    26 appropriate command:
    27 <PRE>
    28 	use "ex/LK/ROOT.ML";
    29 	use "ex/ILL/ROOT.ML";
    30 	use "ex/Modal/ROOT.ML";
    31 </PRE>
    32 </DL>
    33 
    34 <P>Much of the work in Modal logic was done by Martin Coen. Thanks to
    35 Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
    36 reorganized the files and supplied Linear Logic. Jacob Frost provided
    37 some improvements to the syntax of sequents.
    38 
    39 <P>Useful references on sequent calculi:
    40 
    41 <UL>
    42 <LI>Steve Reeves and Michael Clarke,<BR>
    43     Logic for Computer Science (Addison-Wesley, 1990)
    44 <LI>G. Takeuti,<BR>
    45     Proof Theory (North Holland, 1987)
    46 </UL>
    47 
    48 Useful references on Modal Logics:
    49 <UL>
    50 <LI>Melvin C Fitting,<BR>
    51     Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
    52 
    53 <LI>Lincoln A. Wallen,<BR>
    54     Automated Deduction in Nonclassical Logics (MIT Press, 1990)
    55 </UL>
    56 
    57 Useful references on Linear Logic:
    58 <UL>
    59 <LI>A. S. Troelstra<BR>
    60     Lectures on Linear Logic (CSLI, 1992)
    61 
    62 <LI>S. Kalvala and V. de Paiva<BR>
    63     Linear Logic in Isabelle (in TR 379, University of Cambridge
    64 				Computer Lab, 1995, ed L. Paulson)
    65 </UL>
    66 </UL>
    67 </BODY></HTML>