src/Sequents/ROOT
author wenzelm
Mon, 30 Oct 2017 20:04:10 +0100
changeset 66946 3d8fd98c7c86
parent 55229 08f2ebb65078
child 69277 15e9ed5b28fb
permissions -rw-r--r--
ROOT cleanup: empty 'document_files' means there is no document;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
51397
03b586ee5930 support for 'chapter' specifications within session ROOT;
wenzelm
parents: 48738
diff changeset
     1
chapter Sequents
03b586ee5930 support for 'chapter' specifications within session ROOT;
wenzelm
parents: 48738
diff changeset
     2
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48483
diff changeset
     3
session Sequents = Pure +
48475
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
     4
  description {*
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
     5
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
     6
    Copyright   1991  University of Cambridge
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
     7
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     8
    Various Sequent Calculi for Classical, Linear, and Modal Logic.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     9
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    10
    Much of the work in Modal logic was done by Martin Coen. Thanks to Rajeev
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    11
    Gore' for supplying the inference system for S43. Sara Kalvala reorganized
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    12
    the files and supplied Linear Logic. Jacob Frost provided some improvements
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    13
    to the syntax of sequents.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    14
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    15
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    16
    Useful references on sequent calculi:
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    17
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    18
    Steve Reeves and Michael Clarke, Logic for Computer Science
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    19
    (Addison-Wesley, 1990)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    20
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    21
    G. Takeuti, Proof Theory (North Holland, 1987)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    22
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    23
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    24
    Useful references on Modal Logics:
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    25
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    26
    Melvin C Fitting, Proof Methods for Modal and Intuitionistic Logics
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    27
    (Reidel, 1983)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    28
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    29
    Lincoln A. Wallen, Automated Deduction in Nonclassical Logics (MIT Press,
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    30
    1990)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    31
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    32
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    33
    Useful references on Linear Logic:
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    34
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    35
    A. S. Troelstra, Lectures on Linear Logic (CSLI, 1992)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    36
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    37
    S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    38
    of Cambridge Computer Lab, 1995, ed L. Paulson)
48475
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
    39
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    40
  theories
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    41
    LK
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    42
    ILL
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    43
    ILL_predlog
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    44
    Washing
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    45
    Modal0
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    46
    T
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    47
    S4
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    48
    S43
48475
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
    49
55229
08f2ebb65078 simplified sessions;
wenzelm
parents: 51403
diff changeset
    50
    (* Examples for Classical Logic *)
08f2ebb65078 simplified sessions;
wenzelm
parents: 51403
diff changeset
    51
    "LK/Propositional"
08f2ebb65078 simplified sessions;
wenzelm
parents: 51403
diff changeset
    52
    "LK/Quantifiers"
08f2ebb65078 simplified sessions;
wenzelm
parents: 51403
diff changeset
    53
    "LK/Hard_Quantifiers"
08f2ebb65078 simplified sessions;
wenzelm
parents: 51403
diff changeset
    54
    "LK/Nat"