src/Sequents/ROOT
author wenzelm
Sat Jun 02 22:40:03 2018 +0200 (17 months ago)
changeset 68358 e761afd35baa
parent 66946 3d8fd98c7c86
child 69272 15e9ed5b28fb
permissions -rw-r--r--
tuned proofs;
wenzelm@51397
     1
chapter Sequents
wenzelm@51397
     2
wenzelm@48738
     3
session Sequents = Pure +
wenzelm@48475
     4
  description {*
wenzelm@48475
     5
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@48475
     6
    Copyright   1991  University of Cambridge
wenzelm@48475
     7
wenzelm@51403
     8
    Various Sequent Calculi for Classical, Linear, and Modal Logic.
wenzelm@51403
     9
wenzelm@51403
    10
    Much of the work in Modal logic was done by Martin Coen. Thanks to Rajeev
wenzelm@51403
    11
    Gore' for supplying the inference system for S43. Sara Kalvala reorganized
wenzelm@51403
    12
    the files and supplied Linear Logic. Jacob Frost provided some improvements
wenzelm@51403
    13
    to the syntax of sequents.
wenzelm@51403
    14
wenzelm@51403
    15
wenzelm@51403
    16
    Useful references on sequent calculi:
wenzelm@51403
    17
wenzelm@51403
    18
    Steve Reeves and Michael Clarke, Logic for Computer Science
wenzelm@51403
    19
    (Addison-Wesley, 1990)
wenzelm@51403
    20
wenzelm@51403
    21
    G. Takeuti, Proof Theory (North Holland, 1987)
wenzelm@51403
    22
wenzelm@51403
    23
wenzelm@51403
    24
    Useful references on Modal Logics:
wenzelm@51403
    25
wenzelm@51403
    26
    Melvin C Fitting, Proof Methods for Modal and Intuitionistic Logics
wenzelm@51403
    27
    (Reidel, 1983)
wenzelm@51403
    28
wenzelm@51403
    29
    Lincoln A. Wallen, Automated Deduction in Nonclassical Logics (MIT Press,
wenzelm@51403
    30
    1990)
wenzelm@51403
    31
wenzelm@51403
    32
wenzelm@51403
    33
    Useful references on Linear Logic:
wenzelm@51403
    34
wenzelm@51403
    35
    A. S. Troelstra, Lectures on Linear Logic (CSLI, 1992)
wenzelm@51403
    36
wenzelm@51403
    37
    S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
wenzelm@51403
    38
    of Cambridge Computer Lab, 1995, ed L. Paulson)
wenzelm@48475
    39
  *}
wenzelm@48483
    40
  theories
wenzelm@48483
    41
    LK
wenzelm@48483
    42
    ILL
wenzelm@48483
    43
    ILL_predlog
wenzelm@48483
    44
    Washing
wenzelm@48483
    45
    Modal0
wenzelm@48483
    46
    T
wenzelm@48483
    47
    S4
wenzelm@48483
    48
    S43
wenzelm@48475
    49
wenzelm@55229
    50
    (* Examples for Classical Logic *)
wenzelm@55229
    51
    "LK/Propositional"
wenzelm@55229
    52
    "LK/Quantifiers"
wenzelm@55229
    53
    "LK/Hard_Quantifiers"
wenzelm@55229
    54
    "LK/Nat"