A PVS Prover Strategy Package for Common Manipulations

Sequent manipulations for an interactive prover such as PVS can often be labor intensive. We describe an approach to tactic-based proving for improved interactive deduction in specialized domains. An experimental package of strategies (tactics) and support functions has been developed for PVS to reduce the tedium of arithmetic manipulation. Included are strategies aimed at algebraic simplification of real-valued expressions as well as term-access techniques applicable in arbitrary settings. The approach is general enough to serve in other mathematical domains and for provers other than PVS. This report presents the full set of arithmetic strategies and discusses how they are invoked within the prover. Included is a description of the extended expression notation for accessing terms as well as a substitution technique provided for higher-order strategies. Several sample proofs are displayed in full to show how the strategies might be used in practice.