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 by Stephen J. Garland
and John V. Guttag at the MIT Laboratory for Computer Science. It is currently
maintained by Stephen J. Garland.
For a general introduction to LP, see the following topics.
The entire set of pages describing LP is also available as a single, printable