To: larch-interest@src.dec.com Subject: Release 3.1 of LP, the Larch Prover Date: Tue, 03 Jan 95 14:51:50 -0500 From: "Stephen J. Garland" X-Mts: smtp 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.