Index of /ports/math/isabelle/work/Isabelle/src/FOL
Name Last modified Size Description
![[DIR]](/icons/back.gif)
Parent Directory 09-Aug-2008 06:09 -
![[ ]](/icons/unknown.gif)
FOL.ML 27-Nov-2001 15:37 1k
![[TXT]](/icons/text.gif)
FOL.ML.html 09-Aug-2008 06:09 0k
FOL.thy 17-Jun-2005 07:15 4k
FOL.thy.html 09-Aug-2008 06:09 0k
FOL_lemmas1.ML 06-Jul-2000 04:28 3k
FOL_lemmas1.ML.html 09-Aug-2008 06:09 0k
IFOL.ML 25-Aug-1999 11:45 1k
IFOL.ML.html 09-Aug-2008 06:09 0k
IFOL.thy 28-Sep-2005 15:58 7k
IFOL.thy.html 09-Aug-2008 06:09 0k
IFOL_lemmas.ML 07-Apr-2005 00:25 13k
IFOL_lemmas.ML.html 09-Aug-2008 06:09 0k
IsaMakefile 14-Jul-2005 10:28 1k
IsaMakefile.html 09-Aug-2008 06:09 3k
ROOT.ML 20-Jun-2005 13:13 1k
ROOT.ML.html 09-Aug-2008 06:09 0k
blastdata.ML 12-Jul-2005 03:49 1k
blastdata.ML.html 09-Aug-2008 06:09 0k
cladata.ML 20-Aug-2003 02:04 2k
cladata.ML.html 09-Aug-2008 06:09 0k
![[DIR]](/icons/folder.gif)
document/ 09-Aug-2008 06:09 -
eqrule_FOL_data.ML 20-Sep-2005 07:17 2k
eqrule_FOL_data.ML.html 09-Aug-2008 06:09 0k
ex/ 09-Aug-2008 06:09 -
fologic.ML 04-Oct-2001 05:49 3k
fologic.ML.html 09-Aug-2008 06:09 0k
hypsubstdata.ML 03-Dec-2001 17:00 1k
hypsubstdata.ML.html 09-Aug-2008 06:09 0k
intprover.ML 19-Sep-2005 23:21 3k
intprover.ML.html 09-Aug-2008 06:09 0k
simpdata.ML 12-Sep-2005 09:23 12k
simpdata.ML.html 09-Aug-2008 06:09 0k
FOL/README
FOL: First-Order Logic with Natural Deduction
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.
The ex subdirectory contains some examples.
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)