src/Sequents/README.html
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 36862 952b2b102a0a
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; 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
15582
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     3
<HTML>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     4
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     5
<HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     6
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     7
  <TITLE>Sequents/README</TITLE>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     8
</HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     9
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
    10
<BODY>
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    11
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    12
<H2>Sequents: Various Sequent Calculi</H2>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    13
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 2073
diff changeset
    14
This directory contains the ML sources of the Isabelle system for
815ef5848324 tuned all READMEs;
wenzelm
parents: 2073
diff changeset
    15
various Sequent, Linear, and Modal Logic.<p>
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    16
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 2073
diff changeset
    17
The subdirectories <tt>ex</tt>, <tt>ex/LK</tt>, <tt>ex/ILL</tt>,
815ef5848324 tuned all READMEs;
wenzelm
parents: 2073
diff changeset
    18
<tt>ex/Modal</tt> contain some examples.<p>
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    19
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 2073
diff changeset
    20
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
    21
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
    22
reorganized the files and supplied Linear Logic. Jacob Frost provided
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    23
some improvements to the syntax of sequents.
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    24
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    25
<P>Useful references on sequent calculi:
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
<UL>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    28
<LI>Steve Reeves and Michael Clarke,<BR>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    29
    Logic for Computer Science (Addison-Wesley, 1990)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    30
<LI>G. Takeuti,<BR>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    31
    Proof Theory (North Holland, 1987)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    32
</UL>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    33
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    34
Useful references on Modal Logics:
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    35
<UL>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    36
<LI>Melvin C Fitting,<BR>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    37
    Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    38
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    39
<LI>Lincoln A. Wallen,<BR>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    40
    Automated Deduction in Nonclassical Logics (MIT Press, 1990)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    41
</UL>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    42
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    43
Useful references on Linear Logic:
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    44
<UL>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    45
<LI>A. S. Troelstra<BR>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    46
    Lectures on Linear Logic (CSLI, 1992)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    47
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    48
<LI>S. Kalvala and V. de Paiva<BR>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    49
    Linear Logic in Isabelle (in TR 379, University of Cambridge
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    50
				Computer Lab, 1995, ed L. Paulson)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    51
</UL>
5383
74c2da44d144 weblinted, tuned;
wenzelm
parents: 3279
diff changeset
    52
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    53
</BODY></HTML>