src/Sequents/README.html
author wenzelm
Wed May 21 17:13:00 1997 +0200 (1997-05-21)
changeset 3279 815ef5848324
parent 2073 fb0655539d05
child 5383 74c2da44d144
permissions -rw-r--r--
tuned all READMEs;
paulson@2073
     1
<!-- $Id$ -->
wenzelm@3279
     2
<HTML><HEAD><TITLE>Sequents/README</TITLE></HEAD><BODY>
paulson@2073
     3
paulson@2073
     4
<H2>Sequents: Various Sequent Calculi</H2>
paulson@2073
     5
wenzelm@3279
     6
This directory contains the ML sources of the Isabelle system for
wenzelm@3279
     7
various Sequent, Linear, and Modal Logic.<p>
paulson@2073
     8
wenzelm@3279
     9
The subdirectories <tt>ex</tt>, <tt>ex/LK</tt>, <tt>ex/ILL</tt>,
wenzelm@3279
    10
<tt>ex/Modal</tt> contain some examples.<p>
paulson@2073
    11
wenzelm@3279
    12
Much of the work in Modal logic was done by Martin Coen. Thanks to
paulson@2073
    13
Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
paulson@2073
    14
reorganized the files and supplied Linear Logic. Jacob Frost provided
paulson@2073
    15
some improvements to the syntax of sequents.
paulson@2073
    16
paulson@2073
    17
<P>Useful references on sequent calculi:
paulson@2073
    18
paulson@2073
    19
<UL>
paulson@2073
    20
<LI>Steve Reeves and Michael Clarke,<BR>
paulson@2073
    21
    Logic for Computer Science (Addison-Wesley, 1990)
paulson@2073
    22
<LI>G. Takeuti,<BR>
paulson@2073
    23
    Proof Theory (North Holland, 1987)
paulson@2073
    24
</UL>
paulson@2073
    25
paulson@2073
    26
Useful references on Modal Logics:
paulson@2073
    27
<UL>
paulson@2073
    28
<LI>Melvin C Fitting,<BR>
paulson@2073
    29
    Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
paulson@2073
    30
paulson@2073
    31
<LI>Lincoln A. Wallen,<BR>
paulson@2073
    32
    Automated Deduction in Nonclassical Logics (MIT Press, 1990)
paulson@2073
    33
</UL>
paulson@2073
    34
paulson@2073
    35
Useful references on Linear Logic:
paulson@2073
    36
<UL>
paulson@2073
    37
<LI>A. S. Troelstra<BR>
paulson@2073
    38
    Lectures on Linear Logic (CSLI, 1992)
paulson@2073
    39
paulson@2073
    40
<LI>S. Kalvala and V. de Paiva<BR>
paulson@2073
    41
    Linear Logic in Isabelle (in TR 379, University of Cambridge
paulson@2073
    42
				Computer Lab, 1995, ed L. Paulson)
paulson@2073
    43
</UL>
paulson@2073
    44
</UL>
paulson@2073
    45
</BODY></HTML>