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> |
|