[Prev][Next][Index]
Release 3.1 of LP, the Larch Prover
Release 3.1 of LP, the Larch Prover, is available now over the WWW or by
anonymous ftp from larch.lcs.mit.edu. The distribution contains on-line
documentation, which can be read using LP or using a Web browser such as
Mosaic.
To get instructions for obtaining, installing, and using LP, read the WWW
document with URL
http:://larch.lcs.mit.edu:8001/larch/LP/overview.html
or fetch the file
pub/Larch/lp/README
by anonymous ftp from larch.lcs.mit.edu.
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. The following features have been added
to LP since Release 2.4.
o Support for full first-order logic. Earlier releases provided support only
for universal-existential formulas.
o A simple sort system for describing polymorphic abstractions.
o New inference mechanisms, for example, proofs by well founded induction.
o Richer syntactic conventions, such as x[n] and n!, for operators and terms.
o Additional user amenities, for example, enhanced facilities for naming sets
of statements.
LP's on-line information provides complete details about these and other
features of LP.