NASA logo

+ Contact NASA

  • + HOME
  • + TEAM
  • + LINKS

  • 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:

    Package files (for PVS prior to 5.0):

    Other documentation:

    Other items of interest:

    The tag [*] identifies links that are outside the NASA domain