1 <HTML><HEAD><TITLE>FOL/README</TITLE></HEAD><BODY> |
1 <html><head><title>FOL/README</title></head><body> |
2 |
2 |
3 <H2>FOL: First-Order Logic with Natural Deduction</H2> |
3 <h2>FOL: First-Order Logic with Natural Deduction</h2> |
4 |
4 |
5 This directory contains the ML sources of the Isabelle system for |
5 This directory contains the ML sources of the Isabelle system for |
6 First-Order Logic (constructive and classical versions). For a |
6 First-Order Logic (constructive and classical versions). For a |
7 classical sequent calculus, see LK.<p> |
7 classical sequent calculus, see LK.<p> |
8 |
8 |
9 The <tt>ex</tt> subdirectory contains some examples.<p> |
9 The <tt>ex</tt> subdirectory contains some examples.<p> |
10 |
10 |
11 Useful references on First-Order Logic: |
11 Useful references on First-Order Logic: |
12 |
12 |
13 <UL> |
13 <ul> |
14 <LI> Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, 1991)<br> |
14 <li>Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, 1991)<br> |
15 (The first chapter is an excellent introduction to natural |
15 (The first chapter is an excellent introduction to natural |
16 deduction in general.) |
16 deduction in general.) |
17 <LI>Antony Galton, Logic for Information Technology (Wiley, 1990) |
17 <li>Antony Galton, Logic for Information Technology (Wiley, 1990) |
18 <LI>Michael Dummett, Elements of Intuitionism (Oxford, 1977) |
18 <li>Michael Dummett, Elements of Intuitionism (Oxford, 1977) |
19 </UL> |
19 </ul> |
20 </BODY></HTML> |
20 </body></html> |