src/FOL/ROOT
changeset 51403 2ff3a5589b05
parent 51397 03b586ee5930
child 51558 91f8bed6d0a4
equal deleted inserted replaced
51402:b05cd411d3d3 51403:2ff3a5589b05
     1 chapter FOL
     1 chapter FOL
     2 
     2 
     3 session FOL = Pure +
     3 session FOL = Pure +
     4   description "First-Order Logic with Natural Deduction"
     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   *}
     5   options [proofs = 2]
    18   options [proofs = 2]
     6   theories FOL
    19   theories FOL
     7   files "document/root.tex"
    20   files "document/root.tex"
     8 
    21 
     9 session "FOL-ex" in ex = FOL +
    22 session "FOL-ex" in ex = FOL +
       
    23   description {*
       
    24     Examples for First-Order Logic.
       
    25   *}
    10   theories
    26   theories
    11     First_Order_Logic
    27     First_Order_Logic
    12     Natural_Numbers
    28     Natural_Numbers
    13     Intro
    29     Intro
    14     Nat
    30     Nat