SRC Research Report 82

A Guide to LP, The Larch Prover

Stephen J. Garland and John V. Guttag

This guide provides an introduction to LP (the Larch Prover), Release 2.2. It describes how LP can be used to axiomatize theories in a subset of multisorted first-order logic and to provide assistance in proving theorems. It also contains a tutorial overview of the equational term-rewriting technology that provides, along with induction rules and other user-supplied nonequational rules of inference, part of LP's inference engine.

Back to the SRC Research Reports main page.

• PostScript compressed with UNIX compress -- 192 Kbytes
  
• PostScript compressed with GNU compress (gzip) -- 152 Kbytes
  
• PostScript compressed with ZIP -- 152 Kbytes
  
• PostScript -- 416 Kbytes
  
• Portable Document Format (PDF) -- 464 Kbytes