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