Manip: A Strategy Package for PVS

Sequent manipulations for an interactive prover such as PVS can be labor intensive. This unsatisfying situation has prompted our research into tactic-based proving. Our goal is to enhance interactive deduction for specialized domains. Manip is a package of PVS strategies (tactics) developed at NASA Langley Research Center. Although it was designed originally to reduce the tedium of low-level arithmetic manipulation, many of its newer features are suitable as general-purpose prover utilities. Besides strategies aimed at algebraic simplification of real-valued expressions, Manip includes syntax-matching and term-access techniques applicable in arbitrary settings.

Field has been part of PVS since PVS 5.0 and is included in the latest release of PVS.

For higher-level arithmetic simplification, César Muñoz's Field package offers additional automation. Manip can be used as an adjunct to Field to carry out lower-level steps as needed.

Users of PVS 5.0 or higher now have Manip and Field built in to the PVS distribution. No downloads are needed, with the possible exception of the Manip 1.3 User's Manual.

For users of PVS 4.2, NASA Langley's PVS libraries already should have Manip and Field installed as part of the full library distribution. Manip 1.2 is included in the libraries for PVS 4.2.

Current status:

• (18 Apr 2011) Work on Manip 1.3 has been completed. It is now included in the PVS distribution. Any version of PVS from 5.0 on will include the Manip and Field strategy packages. Manip 1.3 will not work with PVS versions earlier than 5.0
• Manip 1.2 (20 Nov 2007) is still the version to use with PVS 4.2 and the NASA libraries. Earlier versions of Manip and PVS are deprecated.
• The 1.1 release of Manip (18 Feb 2003) has been superseded.

Package files (for PVS prior to 5.0):

• Manip version: 1.2, released 20 November 2007
• Requires: PVS 3.1 or higher (Allegro); PVS 4.1 (CMU Lisp)
• Recommended: PVS 4.2
• Installation, history: README
• Documentation (PDF): User's manual (new material in Section 7, p. 34)
• Download (tar.gz): Manip package (includes manual)

Other documentation:

• Technical report, April 2002 (PDF): NASA/TM-2002-211647 (contains most of the version 1.1 user's manual plus additional material on package design considerations along with several proof examples)

Other items of interest:

• César Muñoz's Field package
• NASA Langley's PVS libraries page
• SRI's PVS home page

The tag identifies links that are outside the NASA domain