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