author  haftmann 
Thu, 23 Nov 2017 17:03:27 +0000  
changeset 67087  733017b19de9 
parent 66946  3d8fd98c7c86 
child 69272  15e9ed5b28fb 
permissions  rwrr 
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  4 
description {* 
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 
(AddisonWesley, 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  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  49 

55229  50 
(* Examples for Classical Logic *) 
51 
"LK/Propositional" 

52 
"LK/Quantifiers" 

53 
"LK/Hard_Quantifiers" 

54 
"LK/Nat" 