Manip user’s guide, version 1.3. Sequent manipulations for an interactive prover such as PVS can be labor intensive. We provide an approach to tactic-based proving for improved interactive deduction in specialized domains. This approach has been mechanized by the Manip package of strategies (tactics) and support functions. 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 simpli cation of real-valued expressions, Manip includes term-access techniques applicable in arbitrary settings.
Keywords for this software
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
- Muñoz, César; Narkawicz, Anthony: Formalization of Bernstein polynomials and applications to global optimization (2013)