1chapter Sequents
2
3session Sequents = Pure +
4  description "
5    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
6    Copyright   1991  University of Cambridge
7
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)
39  "
40  directories "LK"
41  theories
42    LK
43    ILL
44    ILL_predlog
45    Washing
46    Modal0
47    T
48    S4
49    S43
50    (* Examples for Classical Logic *)
51    "LK/Propositional"
52    "LK/Quantifiers"
53    "LK/Hard_Quantifiers"
54    "LK/Nat"
55