LP, the Larch Prover -- Introduction
LP is an interactive theorem proving system for multisorted first-order logic.
It is currently used at MIT and elsewhere to reason about designs for circuits,
concurrent algorithms, hardware, and software. Unlike most theorem provers,
which attempt to find proofs automatically for correctly stated conjectures, LP
is intended to assist users in finding and correcting flaws in
conjectures---the predominant activity in the early stages of the design
LP works efficiently on large problems, has many important user amenities, and
can be used by relatively naive users. It was developed and is being
maintained by Stephen J. Garland and John V. Guttag at the MIT Laboratory for
For a general introduction to LP, see the following topics.
This is a preliminary version of the documentation for LP. A more polished
version, both in hypertext and in hardcopy, will be available in early 1995.