author lcp
Tue, 21 Jun 1994 17:20:34 +0200
changeset 435 ca5356bd315a
parent 0 a5a9c433f639
permissions -rw-r--r--
Addition of cardinals and order types, various tidying

		LK: Classical First-Order Sequent Calculus

This directory contains the Standard ML sources of the Isabelle system for
First-Order Logic as a classical sequent calculus.  (For a Natural Deduction
version, see FOL.)  Important files include

ROOT.ML -- loads all source files.  Enter an ML image containing Pure
Isabelle and type:    use "ROOT.ML";

Makefile -- compiles the files under Poly/ML or SML of New Jersey

ex -- subdirectory containing examples.  To execute them, enter an ML image
containing LK and type:    use "ex/ROOT.ML";

Useful references on sequent calculi:

	Jean Gallier, Logic for Computer Science (Harper&Row, 1986)

	G. Takeuti, Proof Theory (North Holland, 1987)