3 session Sequents = Pure + |
3 session Sequents = Pure + |
4 description {* |
4 description {* |
5 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
5 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
6 Copyright 1991 University of Cambridge |
6 Copyright 1991 University of Cambridge |
7 |
7 |
8 Classical Sequent Calculus based on Pure Isabelle. |
8 Various Sequent Calculi for Classical, Linear, and Modal Logic. |
|
9 |
|
10 Much of the work in Modal logic was done by Martin Coen. Thanks to Rajeev |
|
11 Gore' for supplying the inference system for S43. Sara Kalvala reorganized |
|
12 the files and supplied Linear Logic. Jacob Frost provided some improvements |
|
13 to the syntax of sequents. |
|
14 |
|
15 |
|
16 Useful references on sequent calculi: |
|
17 |
|
18 Steve Reeves and Michael Clarke, Logic for Computer Science |
|
19 (Addison-Wesley, 1990) |
|
20 |
|
21 G. Takeuti, Proof Theory (North Holland, 1987) |
|
22 |
|
23 |
|
24 Useful references on Modal Logics: |
|
25 |
|
26 Melvin C Fitting, Proof Methods for Modal and Intuitionistic Logics |
|
27 (Reidel, 1983) |
|
28 |
|
29 Lincoln A. Wallen, Automated Deduction in Nonclassical Logics (MIT Press, |
|
30 1990) |
|
31 |
|
32 |
|
33 Useful references on Linear Logic: |
|
34 |
|
35 A. S. Troelstra, Lectures on Linear Logic (CSLI, 1992) |
|
36 |
|
37 S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University |
|
38 of Cambridge Computer Lab, 1995, ed L. Paulson) |
9 *} |
39 *} |
10 options [document = false] |
40 options [document = false] |
11 theories |
41 theories |
12 LK |
42 LK |
13 ILL |
43 ILL |