src/Sequents/ROOT
author wenzelm
Sat, 29 Feb 2020 17:16:17 +0100
changeset 71497 a80fa14bccb8
parent 70675 efd995488228
child 75992 1f6d79b62222
permissions -rw-r--r--
more Isabelle/jEdit actions;
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 +
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
     4
  description "
48475
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)
69319
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
    39
  "
70675
efd995488228 declare session directories;
wenzelm
parents: 69319
diff changeset
    40
  directories "LK"
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    41
  theories
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    42
    LK
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    43
    ILL
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    44
    ILL_predlog
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    45
    Washing
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    46
    Modal0
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    47
    T
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    48
    S4
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    49
    S43
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"