author | wenzelm |
Fri, 03 Aug 2007 16:28:22 +0200 | |
changeset 24143 | 90a9a6fe0d01 |
parent 15582 | 7219facb3fd0 |
child 36862 | 952b2b102a0a |
permissions | -rw-r--r-- |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> <!-- $Id$ --> <html> <head> <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> <title>FOL/README</title> </head> <body> <h2>FOL: First-Order Logic with Natural Deduction</h2> This directory contains the ML sources of the Isabelle system for First-Order Logic (constructive and classical versions). For a classical sequent calculus, see LK.<p> The <tt>ex</tt> subdirectory contains some examples.<p> Useful references on First-Order Logic: <ul> <li>Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, 1991)<br> (The first chapter is an excellent introduction to natural deduction in general.) <li>Antony Galton, Logic for Information Technology (Wiley, 1990) <li>Michael Dummett, Elements of Intuitionism (Oxford, 1977) </ul> </body> </html>