author | wenzelm |
Sat, 04 Aug 2012 18:05:14 +0200 | |
changeset 48674 | 03e88e4619a2 |
parent 36862 | 952b2b102a0a |
permissions | -rw-r--r-- |
15283 | 1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
2 |
||
15582 | 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> |
|
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 | 14 |
This directory contains the ML sources of the Isabelle system for |
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 | 17 |
The subdirectories <tt>ex</tt>, <tt>ex/LK</tt>, <tt>ex/ILL</tt>, |
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 | 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 | 52 |
|
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset
|
53 |
</BODY></HTML> |