src/FOL/ROOT

author | wenzelm |

Mon, 07 Oct 2013 21:24:44 +0200 | |

changeset 54313 | da2e6282a4f5 |

parent 52488 | cd65ee49a8ba |

child 56781 | f2eb0f22589f |

permissions | -rw-r--r-- |

native executable even for Linux, to avoid surprises with file managers opening executable script as text file;

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 FOL files "document/root.tex" session "FOL-ex" in ex = FOL + description {* Examples for First-Order Logic. *} theories First_Order_Logic 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" files "document/root.tex"