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