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