wenzelm@3279: FOL/README clasohm@1331: clasohm@1331:

FOL: First-Order Logic with Natural Deduction

clasohm@1331: wenzelm@3279: This directory contains the ML sources of the Isabelle system for wenzelm@3279: First-Order Logic (constructive and classical versions). For a wenzelm@3279: classical sequent calculus, see LK.

clasohm@1331: wenzelm@3279: The ex subdirectory contains some examples.

clasohm@1331: clasohm@1331: Useful references on First-Order Logic: clasohm@1331: clasohm@1331:

clasohm@1331: