| author | wenzelm |
| Mon, 24 Oct 2016 15:00:13 +0200 | |
| changeset 64375 | 74a2af7c5145 |
| parent 61935 | 6512e84cc9f5 |
| child 65374 | a5b38d8d3c1e |
| permissions | -rw-r--r-- |
|
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 |
First-Order 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 First-Order 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 (Addison-Wesley, |
|
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 |
*} |
|
56801
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56781
diff
changeset
|
18 |
global_theories |
|
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56781
diff
changeset
|
19 |
IFOL |
|
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56781
diff
changeset
|
20 |
FOL |
|
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 "FOL-ex" 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 First-Order 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 |