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.

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:

Package files (for PVS prior to 5.0):

Other documentation:

Other items of interest:

Note: The link to external site tag identifies links that are outside of the NASA domain.

Manip is now quite mature. It has been exercised successfully for nearly ten years by users at NASA Langley and also at a few other sites. Further development in the near future is not anticipated, although enhancements are possible if the need arises. Feedback of any kind is still encouraged. We also welcome users to build on these features when developing their own personal strategies.

Ben L. Di Vito :

Curator and Responsible NASA Official: Ben L. Di Vito
LaRC privacy statement
Last modified: 27 July 2011