src/FOL/ROOT
 author blanchet Mon Sep 15 10:49:07 2014 +0200 (2014-09-15) changeset 58335 a5a3b576fcfb parent 56801 8dd9df88f647 child 61935 6512e84cc9f5 permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
```     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   global_theories
```
```    19     IFOL
```
```    20     FOL
```
```    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     First_Order_Logic
```
```    29     Natural_Numbers
```
```    30     Intro
```
```    31     Nat
```
```    32     Nat_Class
```
```    33     Foundation
```
```    34     Prolog
```
```    35     Intuitionistic
```
```    36     Propositional_Int
```
```    37     Quantifiers_Int
```
```    38     Classical
```
```    39     Propositional_Cla
```
```    40     Quantifiers_Cla
```
```    41     Miniscope
```
```    42     If
```
```    43   theories [document = false, skip_proofs = false]
```
```    44     "Locale_Test/Locale_Test"
```
```    45   document_files "root.tex"
```
```    46
```