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