@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%