src/Sequents/README.html
author oheimb
Wed, 12 Nov 1997 18:58:50 +0100
changeset 4223 f60e3d2c81d3
parent 3279 815ef5848324
child 5383 74c2da44d144
permissions -rw-r--r--
added thin_refl to hyp_subst_tac

<!-- $Id$ -->
<HTML><HEAD><TITLE>Sequents/README</TITLE></HEAD><BODY>

<H2>Sequents: Various Sequent Calculi</H2>

This directory contains the ML sources of the Isabelle system for
various Sequent, Linear, and Modal Logic.<p>

The subdirectories <tt>ex</tt>, <tt>ex/LK</tt>, <tt>ex/ILL</tt>,
<tt>ex/Modal</tt> contain some examples.<p>

Much of the work in Modal logic was done by Martin Coen. Thanks to
Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
reorganized the files and supplied Linear Logic. Jacob Frost provided
some improvements to the syntax of sequents.

<P>Useful references on sequent calculi:

<UL>
<LI>Steve Reeves and Michael Clarke,<BR>
    Logic for Computer Science (Addison-Wesley, 1990)
<LI>G. Takeuti,<BR>
    Proof Theory (North Holland, 1987)
</UL>

Useful references on Modal Logics:
<UL>
<LI>Melvin C Fitting,<BR>
    Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)

<LI>Lincoln A. Wallen,<BR>
    Automated Deduction in Nonclassical Logics (MIT Press, 1990)
</UL>

Useful references on Linear Logic:
<UL>
<LI>A. S. Troelstra<BR>
    Lectures on Linear Logic (CSLI, 1992)

<LI>S. Kalvala and V. de Paiva<BR>
    Linear Logic in Isabelle (in TR 379, University of Cambridge
				Computer Lab, 1995, ed L. Paulson)
</UL>
</UL>
</BODY></HTML>