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