@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Name: LP, the Larch Prover Keywords: equational term rewriting, induction Description: Semantics: first-order logic Deductive machinery: equational term rewriting, induction Dynamics: interactive mode for proof development; replay mode for proof maintenance Persistence: proof scripts, theories, proof development states, proof logs User supplies: equations (LP provides help in orienting them into terminating rewrite rules) assertions about operators (commutative, associative-commutative) deduction rules (equivalent to universal-existential formulas) induction schemes explicit proof guidance ordering hints (optional) Inference rules: forward rules reduction of known facts to normal form (using rewrite rules) deduction (using deduction rules) instantiation critical pairs (also used in Knuth-Bendix completion) backward rules (to prove or generate subgoals from conjectures) reduction induction proofs by cases, contradiction proofs of conditionals, implications proofs of deduction and induction rules proofs of assertions about operators Facilities for naming objects, sets of objects, logging and replaying input, generating transcripts, checkpointing. LP is designed for a middle ground between proof checkers that require detailed guidance and theorem provers that work completely automatically. It allows the user to direct the proof process at a fairly high level, with the goal that the ``obvious'' steps will be taken automatically. LP's design is based on the assumption that initial attempts to state conjectures correctly, and then prove them, usually fail. As a result, LP is designed to carry out routine (and possibly lengthy) steps in a proof automatically and to provide useful information about why proofs fail, if and when they do. LP is not designed to find difficult proofs automatically; instead, LP makes it easy for users to employ standard techniques such as proofs by cases, induction, and contradiction. It can be used interactively to debug conjectures and proofs, or in a batch mode to maintain existing proofs. Contact persons: garland@lcs.mit.edu guttag@lcs.mit.edu User group: larch-interest@pa.dec.com Pragmatics: Works better for ``large'' proofs (big formulas and/or many facts), rather than for deep ones. Documentation: 90-page user guide: S.J. Garland and J.V. Guttag. ``A Guide to LP, The Larch Prover,'' DEC Systems Research Center Report 82, 1991. [A PostScript file containing this report is part of the distribution.] Applications: Collections of papers - U. Martin and J.M Wing, ``First International Workshop on Larch,'' Springer-Verlag, 1992. Reasoning about specifications - S.J. Garland, J.V. Guttag, and J.J. Horning, ``Debugging Larch Shared Language Specifications,'' IEEE Transactions on Software Engineering 16:9 (September 1990), 1044-1057. [Also appears as Chapter 7 in Guttag and Horning, Larch: Languages and Tools for Formal Specification, Springer-Verlag, 1993.] - M. Bidoit and R. Hennicker, ``How to prove observational theorems with LP,'' in 1992 Larch Workshop, 18-35. - J.M. Wing, E. Rollins, and A.M. Zaremski, ``Thoughts on a Larch/ML and a new application for LP,'' in 1992 Larch Workshop, 297-312. Reasoning about concurrency - J.F. Soegaard-Anderson, S.J. Garland, J.V. Guttag, N.A. Lynch, and A. Pogosyants, ``Computed-assisted simulation proofs,'' Fourth Conference on Computer-Aided Verification, Lecture Notes in Computer Science 697, Springer-Verlag, 305-319. - U. Engberg, P. Groenning, and L. Lamport, ``Mechanical verification of concurrent systems with TLA,'' in 1992 Larch Workshop, 86-97. Proofs about circuits - S.J. Garland, J.V. Guttag, and J. Staunstrup, ``Verification of VLSI Circuits using LP,'' IFIP WG 10.2 Proceedings, The Fusion of Hardware Design and Verification, North Holland, 1988, 329-345. - J. Staunstrup, S.J. Garland, and J.V. Guttag, ``Localized Verification of Circuit Descriptions," Proceedings of a Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, June 1989, Lecture Notes in Computer Science 407, Springer-Verlag, 349-364. - J.B. Saxe, S.J. Garland, J.V. Guttag, J.J. Horning, ``Using Transformations and Verification in Circuit Design,'' IFIP WG10.2/10.5 Proceedings, Designing Correct Circuits, North Holland IFIP Transactions A-5, 1992, 1-15. [Also in 1992 Larch Workshop, 201-226.] - J. Staunstrup, S.J. Garland, and J.V. Guttag, ``Mechanized Verification of Circuit Descriptions using the Larch Prover,'' IFIP TC10/WG10.2 Proceedings, Theorem Provers in Circuit Design, North-Holland, 1992, 277-300. - N. Mellergaard and J. Staunstrup, ``Generating proof obligations for circuits,'' in 1992 Larch Workshop, 185-200. - B. Chetali and P. Lescanne, ``An exercise in LP: the proof of a nonrestoring division circuit,'' in 1992 Larch Workshop, 55-68. Programming languages - E.A. Scott and K.J. Norrie, ``Using LP to study the language PL^+_0,'' in 1992 Larch Workshop, 227-245. - U. Martin and T. Nipkow, ``Automating Squiggol,'' Proceedings of the Programming Concepts and Methods IFIP TC2 Working Conference, Sea of Galilee, Israel, April 1990, North-Holland, 223-236. Mathematics - U. Martin and M. Lai, ``Some experiments with a completion theorem prover,'' Journal of Symbolic Computation, 1991. Avalon Project - J.M. Wing and C. Gong, ``Experience with the Larch Prover,'' Proceedings of the ACM Workshop on Formal Methods in Software Development, Napa, CA, May 9-11, 1990, 140-143. - C. Gong and J.M. Wing, ``Raw Code, Specification, and Proof of the Avalon Queue Example,'' CMU-CS-89-172, August 1989. - J.M. Wing and C. Gong, ``Machine-Assisted Proofs of Properties of Avalon Programs,'' CMU-CS-89-171, August 1989. Extensions/enhancements: Part of the Larch project for formal specification. Experimental versions provide conditional rewriting and full first-order quantification. Resource requirements: Written in CLU, runs on DEC VAX, DECStation 3100 & 5000, DEC Alpha, SUN Sparcstation, Sun-3. Used at MIT, CMU, DEC SRC, Technical University of Denmark, Aarhus (DK), University of Paris-South, ... Where-to-get-it: No license is required for using LP. LP can be obtained by anonymous ftp from larch.lcs.mit.edu (18.26.0.95). You should use a dialog such as csh>>ftp larch.lcs.mit.edu Name: anonymous Password: ftp> cd pub/Larch ftp> binary ftp> get lp2.4.lib.tar.Z ftp> get lp2.4..Z ftp> quit to get a tar file containing documentation and a runtime library for LP, together with a compressed executable version of LP for one of the following platforms: decmips DEC/MIPS 3100 or 5000 workstations sparc Sun Sparcstations vax DEC VAX computers under Berkeley Unix 4.3 with NFS or a compatible version of Unix such as Ultrix [Info source, date ] garland@lcs.mit.edu, September 10, 1993 pub/Larch/README on larch.lcs.mit.edu, March 26, 1993 CADE 9 1988 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%