chapter FOL
session FOL = Pure +
description {*
First-Order Logic with Natural Deduction (constructive and classical
versions). For a classical sequent calculus, see Isabelle/LK.
Useful references on First-Order Logic:
Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
1991) (The first chapter is an excellent introduction to natural deduction
in general.)
Antony Galton, Logic for Information Technology (Wiley, 1990)
Michael Dummett, Elements of Intuitionism (Oxford, 1977)
*}
theories
IFOL (global)
FOL (global)
document_files "root.tex"
session "FOL-ex" in ex = FOL +
description {*
Examples for First-Order Logic.
*}
theories
Natural_Numbers
Intro
Nat
Nat_Class
Foundation
Prolog
Intuitionistic
Propositional_Int
Quantifiers_Int
Classical
Propositional_Cla
Quantifiers_Cla
Miniscope
If
theories [document = false, skip_proofs = false]
"Locale_Test/Locale_Test"
document_files "root.tex"