author | wenzelm |
Mon, 05 Feb 2024 12:59:34 +0100 | |
changeset 79578 | 4c4d71b00001 |
parent 76006 | c9d56340b56e |
permissions | -rw-r--r-- |
75988
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
1 |
chapter_definition HOL |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
2 |
description " |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
3 |
Higher-Order Logic. |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
4 |
|
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
5 |
Isabelle/HOL is a version of classical higher-order logic resembling |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
6 |
that of the HOL System (https://www.cl.cam.ac.uk/Research/HVG/HOL). |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
7 |
" |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
8 |
|
75992 | 9 |
chapter_definition FOL |
75988
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
10 |
description " |
75992 | 11 |
First-Order Logic with some variations: single-sorted vs. many-sorted |
76006
c9d56340b56e
ZF belongs to chapter FOL, following lib/html/library_index_content.template (i.e. "Documentation" area on website);
wenzelm
parents:
76004
diff
changeset
|
12 |
(polymorphic), classical vs. intuitionistic, domain-theory (LCF) vs. |
c9d56340b56e
ZF belongs to chapter FOL, following lib/html/library_index_content.template (i.e. "Documentation" area on website);
wenzelm
parents:
76004
diff
changeset
|
13 |
set-theory (ZF). |
75988
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
14 |
" |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
15 |
|
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
16 |
chapter_definition Pure |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
17 |
description " |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
18 |
The Pure logical framework. |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
19 |
|
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
20 |
Isabelle/Pure is a version of intuitionistic higher-order logic that |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
21 |
expresses rules for Natural Deduction declaratively. |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
22 |
" |
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
23 |
|
75992 | 24 |
chapter_definition Misc |
76000 | 25 |
description " |
26 |
Miscellaneous object-logics, tools, and experiments. |
|
27 |
" |
|
75992 | 28 |
|
75988
ca73ced9e630
provide chapter descriptions, based on lib/html/library_index_content.template;
wenzelm
parents:
diff
changeset
|
29 |
chapter_definition Doc |
76000 | 30 |
description " |
31 |
Sources of Documentation. |
|
32 |
" |
|
76004
152c5c83c119
proper chapter_definition to prevent odd definitions by users;
wenzelm
parents:
76000
diff
changeset
|
33 |
|
152c5c83c119
proper chapter_definition to prevent odd definitions by users;
wenzelm
parents:
76000
diff
changeset
|
34 |
chapter_definition Unsorted |
152c5c83c119
proper chapter_definition to prevent odd definitions by users;
wenzelm
parents:
76000
diff
changeset
|
35 |
description " |
152c5c83c119
proper chapter_definition to prevent odd definitions by users;
wenzelm
parents:
76000
diff
changeset
|
36 |
Sessions without 'chapter' declaration. |
152c5c83c119
proper chapter_definition to prevent odd definitions by users;
wenzelm
parents:
76000
diff
changeset
|
37 |
" |