A Guide to LP: the Larch Prover

Stephen J. Garland and John V. Guttag,

MIT Laboratory for Computer Science, December 1991. Also published as Digital Equipment Corporation Systems Research Center Report 82, 1991.

This guide provides an introduction to LP (the Larch Prover), Release 2.2. It describes how LP can be used to axiomatize theories in a subset of multisorted first-order logic and to provide assistance in proving theorems. It also contains a tutorial overview of the equational term-rewriting technology that provides, along with induction rules and other user-supplied nonequational rules of inference, part of LP's inference engine.

Back to Publications of Stephen J. Garland