| author | Walther Neuper <neuper@ist.tugraz.at> |
| Fri, 01 Oct 2010 17:27:55 +0200 | |
| branch | isac-update-Isa09-2 |
| changeset 38039 | 99cb0d80ff32 |
| parent 36869 | 952b2b102a0a |
| permissions | -rw-r--r-- |
| webertj@15283 | 1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
| webertj@15283 | 2 |
|
| webertj@15582 | 3 |
<html> |
| webertj@15582 | 4 |
|
| webertj@15582 | 5 |
<head> |
| webertj@15582 | 6 |
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
| webertj@15582 | 7 |
<title>FOL/README</title> |
| webertj@15582 | 8 |
</head> |
| webertj@15582 | 9 |
|
| webertj@15582 | 10 |
<body> |
| clasohm@1331 | 11 |
|
| wenzelm@11849 | 12 |
<h2>FOL: First-Order Logic with Natural Deduction</h2> |
| clasohm@1331 | 13 |
|
| wenzelm@3279 | 14 |
This directory contains the ML sources of the Isabelle system for |
| wenzelm@3279 | 15 |
First-Order Logic (constructive and classical versions). For a |
| wenzelm@3279 | 16 |
classical sequent calculus, see LK.<p> |
| clasohm@1331 | 17 |
|
| wenzelm@3279 | 18 |
The <tt>ex</tt> subdirectory contains some examples.<p> |
| clasohm@1331 | 19 |
|
| clasohm@1331 | 20 |
Useful references on First-Order Logic: |
| clasohm@1331 | 21 |
|
| wenzelm@11849 | 22 |
<ul> |
| wenzelm@11849 | 23 |
<li>Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, 1991)<br> |
| wenzelm@11849 | 24 |
(The first chapter is an excellent introduction to natural |
| wenzelm@3279 | 25 |
deduction in general.) |
| wenzelm@11849 | 26 |
<li>Antony Galton, Logic for Information Technology (Wiley, 1990) |
| wenzelm@11849 | 27 |
<li>Michael Dummett, Elements of Intuitionism (Oxford, 1977) |
| wenzelm@11849 | 28 |
</ul> |
| webertj@15582 | 29 |
</body> |
| webertj@15582 | 30 |
</html> |