src/Sequents/README.html
author wenzelm
Mon Mar 19 21:10:33 2012 +0100 (2012-03-19)
changeset 47022 8eac39af4ec0
parent 36862 952b2b102a0a
permissions -rw-r--r--
moved some legacy stuff;
webertj@15283
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
webertj@15283
     2
webertj@15582
     3
<HTML>
webertj@15582
     4
webertj@15582
     5
<HEAD>
webertj@15582
     6
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
webertj@15582
     7
  <TITLE>Sequents/README</TITLE>
webertj@15582
     8
</HEAD>
webertj@15582
     9
webertj@15582
    10
<BODY>
paulson@2073
    11
paulson@2073
    12
<H2>Sequents: Various Sequent Calculi</H2>
paulson@2073
    13
wenzelm@3279
    14
This directory contains the ML sources of the Isabelle system for
wenzelm@3279
    15
various Sequent, Linear, and Modal Logic.<p>
paulson@2073
    16
wenzelm@3279
    17
The subdirectories <tt>ex</tt>, <tt>ex/LK</tt>, <tt>ex/ILL</tt>,
wenzelm@3279
    18
<tt>ex/Modal</tt> contain some examples.<p>
paulson@2073
    19
wenzelm@3279
    20
Much of the work in Modal logic was done by Martin Coen. Thanks to
paulson@2073
    21
Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
paulson@2073
    22
reorganized the files and supplied Linear Logic. Jacob Frost provided
paulson@2073
    23
some improvements to the syntax of sequents.
paulson@2073
    24
paulson@2073
    25
<P>Useful references on sequent calculi:
paulson@2073
    26
paulson@2073
    27
<UL>
paulson@2073
    28
<LI>Steve Reeves and Michael Clarke,<BR>
paulson@2073
    29
    Logic for Computer Science (Addison-Wesley, 1990)
paulson@2073
    30
<LI>G. Takeuti,<BR>
paulson@2073
    31
    Proof Theory (North Holland, 1987)
paulson@2073
    32
</UL>
paulson@2073
    33
paulson@2073
    34
Useful references on Modal Logics:
paulson@2073
    35
<UL>
paulson@2073
    36
<LI>Melvin C Fitting,<BR>
paulson@2073
    37
    Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
paulson@2073
    38
paulson@2073
    39
<LI>Lincoln A. Wallen,<BR>
paulson@2073
    40
    Automated Deduction in Nonclassical Logics (MIT Press, 1990)
paulson@2073
    41
</UL>
paulson@2073
    42
paulson@2073
    43
Useful references on Linear Logic:
paulson@2073
    44
<UL>
paulson@2073
    45
<LI>A. S. Troelstra<BR>
paulson@2073
    46
    Lectures on Linear Logic (CSLI, 1992)
paulson@2073
    47
paulson@2073
    48
<LI>S. Kalvala and V. de Paiva<BR>
paulson@2073
    49
    Linear Logic in Isabelle (in TR 379, University of Cambridge
paulson@2073
    50
				Computer Lab, 1995, ed L. Paulson)
paulson@2073
    51
</UL>
wenzelm@5383
    52
paulson@2073
    53
</BODY></HTML>