author | wenzelm |
Sat, 29 Feb 2020 17:16:17 +0100 | |
changeset 71497 | a80fa14bccb8 |
parent 70675 | efd995488228 |
child 75992 | 1f6d79b62222 |
permissions | -rw-r--r-- |
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 | 4 |
description " |
48475 | 5 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
6 |
Copyright 1991 University of Cambridge |
|
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 | 39 |
" |
70675 | 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 | 50 |
(* Examples for Classical Logic *) |
51 |
"LK/Propositional" |
|
52 |
"LK/Quantifiers" |
|
53 |
"LK/Hard_Quantifiers" |
|
54 |
"LK/Nat" |