author  wenzelm 
Sat, 25 May 2013 17:40:44 +0200  
changeset 52147  9943f8067f11 
parent 51403  2ff3a5589b05 
child 55229  08f2ebb65078 
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 
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  50 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48483
diff
changeset

51 
session "SequentsLK" in LK = Sequents + 
48475  52 
description {* 
53 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

54 
Copyright 1992 University of Cambridge 

55 

56 
Examples for Classical Logic. 

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  64 