author  wenzelm 
Sat, 25 May 2013 17:40:44 +0200  
changeset 52147  9943f8067f11 
parent 51558  91f8bed6d0a4 
child 52488  cd65ee49a8ba 
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 
*} 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

18 
options [proofs = 2] 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

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

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

21 

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

22 
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

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

24 
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

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

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

27 
First_Order_Logic 
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" 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

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

45 