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