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 process.

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.

Getting the current distribution of LP
News about recent changes to LP
Using LP
- Some sample proofs
- Logical syntax and semantics
- Operational syntax and semantics
- Forward inference mechanisms for using axioms
- Backward inference mechanisms for proving conjectures
- Commands recognized by LP
Design philosophy
Table of contents for this documentation

The entire set of pages describing LP is also available as a single, printable document.