src/FOL/ROOT
 author wenzelm Mon Dec 04 22:54:31 2017 +0100 (20 months ago) changeset 67131 85d10959c2e4 parent 65374 a5b38d8d3c1e child 69272 15e9ed5b28fb permissions -rw-r--r--
tuned signature;
```     1 chapter FOL
```
```     2
```
```     3 session FOL = Pure +
```
```     4   description {*
```
```     5     First-Order Logic with Natural Deduction (constructive and classical
```
```     6     versions). For a classical sequent calculus, see Isabelle/LK.
```
```     7
```
```     8     Useful references on First-Order Logic:
```
```     9
```
```    10     Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
```
```    11     1991) (The first chapter is an excellent introduction to natural deduction
```
```    12     in general.)
```
```    13
```
```    14     Antony Galton, Logic for Information Technology (Wiley, 1990)
```
```    15
```
```    16     Michael Dummett, Elements of Intuitionism (Oxford, 1977)
```
```    17   *}
```
```    18   theories
```
```    19     IFOL (global)
```
```    20     FOL (global)
```
```    21   document_files "root.tex"
```
```    22
```
```    23 session "FOL-ex" in ex = FOL +
```
```    24   description {*
```
```    25     Examples for First-Order Logic.
```
```    26   *}
```
```    27   theories
```
```    28     Natural_Numbers
```
```    29     Intro
```
```    30     Nat
```
```    31     Nat_Class
```
```    32     Foundation
```
```    33     Prolog
```
```    34     Intuitionistic
```
```    35     Propositional_Int
```
```    36     Quantifiers_Int
```
```    37     Classical
```
```    38     Propositional_Cla
```
```    39     Quantifiers_Cla
```
```    40     Miniscope
```
```    41     If
```
```    42   theories [document = false, skip_proofs = false]
```
```    43     "Locale_Test/Locale_Test"
```
```    44   document_files "root.tex"
```
```    45
```