src/Sequents/ROOT
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 51403 2ff3a5589b05
child 55229 08f2ebb65078
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
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
  options [document = false]
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
48475
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
    50
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48483
diff changeset
    51
session "Sequents-LK" in LK = Sequents +
48475
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
    52
  description {*
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
    53
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
    54
    Copyright   1992  University of Cambridge
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
    55
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
    56
    Examples for Classical Logic.
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
    57
  *}
48483
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    58
  options [document = false]
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    59
  theories
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    60
    Propositional
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    61
    Quantifiers
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    62
    Hard_Quantifiers
9bfb6978eb80 more explicit document = false to reduce warnings;
wenzelm
parents: 48475
diff changeset
    63
    Nat
48475
02dd825f5a4e more session ROOT files;
wenzelm
parents:
diff changeset
    64