author  wenzelm 
Tue, 04 Apr 2017 21:05:07 +0200  
changeset 65374  a5b38d8d3c1e 
parent 61935  6512e84cc9f5 
child 69272  15e9ed5b28fb 
permissions  rwrr 
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
48738
diff
changeset

1 
chapter FOL 
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:
48487
diff
changeset

3 
session FOL = Pure + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

4 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

5 
FirstOrder Logic with Natural Deduction (constructive and classical 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

6 
versions). For a classical sequent calculus, see Isabelle/LK. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

7 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

8 
Useful references on FirstOrder 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 
Simon Thompson, Type Theory and Functional Programming (AddisonWesley, 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

11 
1991) (The first chapter is an excellent introduction to natural deduction 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

12 
in general.) 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

13 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

14 
Antony Galton, Logic for Information Technology (Wiley, 1990) 
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 
Michael Dummett, Elements of Intuitionism (Oxford, 1977) 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

17 
*} 
65374  18 
theories 
19 
IFOL (global) 

20 
FOL (global) 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
52488
diff
changeset

21 
document_files "root.tex" 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

22 

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

23 
session "FOLex" in ex = FOL + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

24 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

25 
Examples for FirstOrder Logic. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

26 
*} 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

27 
theories 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

28 
Natural_Numbers 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

29 
Intro 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

30 
Nat 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

31 
Nat_Class 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

32 
Foundation 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

33 
Prolog 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

34 
Intuitionistic 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

35 
Propositional_Int 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

36 
Quantifiers_Int 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

37 
Classical 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

38 
Propositional_Cla 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

39 
Quantifiers_Cla 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

40 
Miniscope 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

41 
If 
51558
91f8bed6d0a4
allow build with skip_proofs enabled  disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents:
51403
diff
changeset

42 
theories [document = false, skip_proofs = false] 
91f8bed6d0a4
allow build with skip_proofs enabled  disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents:
51403
diff
changeset

43 
"Locale_Test/Locale_Test" 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
52488
diff
changeset

44 
document_files "root.tex" 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

45 