src/Sequents/ROOT
author wenzelm
Mon Oct 30 20:04:10 2017 +0100 (20 months ago)
changeset 66946 3d8fd98c7c86
parent 55229 08f2ebb65078
child 69272 15e9ed5b28fb
permissions -rw-r--r--
ROOT cleanup: empty 'document_files' means there is no document;
     1 chapter Sequents
     2 
     3 session 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   theories
    41     LK
    42     ILL
    43     ILL_predlog
    44     Washing
    45     Modal0
    46     T
    47     S4
    48     S43
    49 
    50     (* Examples for Classical Logic *)
    51     "LK/Propositional"
    52     "LK/Quantifiers"
    53     "LK/Hard_Quantifiers"
    54     "LK/Nat"