src/Sequents/README.html
changeset 2073 fb0655539d05
child 3279 815ef5848324
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Sequents/README.html	Wed Oct 09 13:32:33 1996 +0200
     1.3 @@ -0,0 +1,67 @@
     1.4 +<!-- $Id$ -->
     1.5 +<HTML><HEAD><TITLE>Sequents/ReadMe</TITLE></HEAD><BODY>
     1.6 +
     1.7 +<H2>Sequents: Various Sequent Calculi</H2>
     1.8 +
     1.9 +This directory contains the Standard ML sources of the Isabelle system for
    1.10 +various Sequent, Linear, and Modal Logic.  Important files include
    1.11 +
    1.12 +<DL>
    1.13 +<DT>ROOT.ML
    1.14 +<DD>loads all source files.  Enter an ML image containing Pure
    1.15 +Isabelle and type:    use "ROOT.ML";
    1.16 +
    1.17 +<DT>Makefile
    1.18 +<DD>compiles the files under Poly/ML or SML of New Jersey
    1.19 +
    1.20 +
    1.21 +<DT>ex
    1.22 +<DD>subdirectory containing examples.  Files are arranged in
    1.23 +subdirectories. To execute all of them, enter an ML image containing
    1.24 +Sequents and type 
    1.25 +<PRE>
    1.26 +	use "ex/ROOT.ML";
    1.27 +</PRE>
    1.28 +To execute examples in a particular logic (LK/ILL/Modal) use the
    1.29 +appropriate command:
    1.30 +<PRE>
    1.31 +	use "ex/LK/ROOT.ML";
    1.32 +	use "ex/ILL/ROOT.ML";
    1.33 +	use "ex/Modal/ROOT.ML";
    1.34 +</PRE>
    1.35 +</DL>
    1.36 +
    1.37 +<P>Much of the work in Modal logic was done by Martin Coen. Thanks to
    1.38 +Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
    1.39 +reorganized the files and supplied Linear Logic. Jacob Frost provided
    1.40 +some improvements to the syntax of sequents.
    1.41 +
    1.42 +<P>Useful references on sequent calculi:
    1.43 +
    1.44 +<UL>
    1.45 +<LI>Steve Reeves and Michael Clarke,<BR>
    1.46 +    Logic for Computer Science (Addison-Wesley, 1990)
    1.47 +<LI>G. Takeuti,<BR>
    1.48 +    Proof Theory (North Holland, 1987)
    1.49 +</UL>
    1.50 +
    1.51 +Useful references on Modal Logics:
    1.52 +<UL>
    1.53 +<LI>Melvin C Fitting,<BR>
    1.54 +    Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
    1.55 +
    1.56 +<LI>Lincoln A. Wallen,<BR>
    1.57 +    Automated Deduction in Nonclassical Logics (MIT Press, 1990)
    1.58 +</UL>
    1.59 +
    1.60 +Useful references on Linear Logic:
    1.61 +<UL>
    1.62 +<LI>A. S. Troelstra<BR>
    1.63 +    Lectures on Linear Logic (CSLI, 1992)
    1.64 +
    1.65 +<LI>S. Kalvala and V. de Paiva<BR>
    1.66 +    Linear Logic in Isabelle (in TR 379, University of Cambridge
    1.67 +				Computer Lab, 1995, ed L. Paulson)
    1.68 +</UL>
    1.69 +</UL>
    1.70 +</BODY></HTML>