|
1 <!-- $Id$ --> |
|
2 <HTML><HEAD><TITLE>Sequents/ReadMe</TITLE></HEAD><BODY> |
|
3 |
|
4 <H2>Sequents: Various Sequent Calculi</H2> |
|
5 |
|
6 This directory contains the Standard ML sources of the Isabelle system for |
|
7 various Sequent, Linear, and Modal Logic. Important files include |
|
8 |
|
9 <DL> |
|
10 <DT>ROOT.ML |
|
11 <DD>loads all source files. Enter an ML image containing Pure |
|
12 Isabelle and type: use "ROOT.ML"; |
|
13 |
|
14 <DT>Makefile |
|
15 <DD>compiles the files under Poly/ML or SML of New Jersey |
|
16 |
|
17 |
|
18 <DT>ex |
|
19 <DD>subdirectory containing examples. Files are arranged in |
|
20 subdirectories. To execute all of them, enter an ML image containing |
|
21 Sequents and type |
|
22 <PRE> |
|
23 use "ex/ROOT.ML"; |
|
24 </PRE> |
|
25 To execute examples in a particular logic (LK/ILL/Modal) use the |
|
26 appropriate command: |
|
27 <PRE> |
|
28 use "ex/LK/ROOT.ML"; |
|
29 use "ex/ILL/ROOT.ML"; |
|
30 use "ex/Modal/ROOT.ML"; |
|
31 </PRE> |
|
32 </DL> |
|
33 |
|
34 <P>Much of the work in Modal logic was done by Martin Coen. Thanks to |
|
35 Rajeev Gore' for supplying the inference system for S43. Sara Kalvala |
|
36 reorganized the files and supplied Linear Logic. Jacob Frost provided |
|
37 some improvements to the syntax of sequents. |
|
38 |
|
39 <P>Useful references on sequent calculi: |
|
40 |
|
41 <UL> |
|
42 <LI>Steve Reeves and Michael Clarke,<BR> |
|
43 Logic for Computer Science (Addison-Wesley, 1990) |
|
44 <LI>G. Takeuti,<BR> |
|
45 Proof Theory (North Holland, 1987) |
|
46 </UL> |
|
47 |
|
48 Useful references on Modal Logics: |
|
49 <UL> |
|
50 <LI>Melvin C Fitting,<BR> |
|
51 Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983) |
|
52 |
|
53 <LI>Lincoln A. Wallen,<BR> |
|
54 Automated Deduction in Nonclassical Logics (MIT Press, 1990) |
|
55 </UL> |
|
56 |
|
57 Useful references on Linear Logic: |
|
58 <UL> |
|
59 <LI>A. S. Troelstra<BR> |
|
60 Lectures on Linear Logic (CSLI, 1992) |
|
61 |
|
62 <LI>S. Kalvala and V. de Paiva<BR> |
|
63 Linear Logic in Isabelle (in TR 379, University of Cambridge |
|
64 Computer Lab, 1995, ed L. Paulson) |
|
65 </UL> |
|
66 </UL> |
|
67 </BODY></HTML> |