author  wenzelm 
Mon, 07 Oct 2013 21:24:44 +0200  
changeset 54313  da2e6282a4f5 
parent 52488  cd65ee49a8ba 
child 56781  f2eb0f22589f 
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 
theories FOL 
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

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

20 

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

21 
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

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

23 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

40 
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

41 
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

42 
"Locale_Test/Locale_Test" 
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset

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

44 