equal
deleted
inserted
replaced
|
1 FOL: First-Order Logic with Natural Deduction |
|
2 |
|
3 This directory contains the Standard ML sources of the Isabelle system for |
|
4 First-Order Logic (constructive and classical versions). For a classical |
|
5 sequent calculus, see LK. Important files include |
|
6 |
|
7 ROOT.ML -- loads all source files. Enter an ML image containing Pure |
|
8 Isabelle and type: use "ROOT.ML"; |
|
9 |
|
10 Makefile -- compiles the files under Poly/ML or SML of New Jersey |
|
11 |
|
12 ex -- subdirectory containing examples. To execute them, enter an ML image |
|
13 containing FOL and type: use "ex/ROOT.ML"; |
|
14 |
|
15 Useful references on First-Order Logic: |
|
16 |
|
17 Antony Galton, Logic for Information Technology (Wiley, 1990) |
|
18 |
|
19 Michael Dummett, Elements of Intuitionism (Oxford, 1977) |