Extrategies is a set of strategy combinators and Lisp functions for writting strategies in PVS. Extrategies also contains improved versions of standard PVS strategies for skolemizing, naming, labeling, replacing, splitting, etc.
Extrategies has been part of PVS since PVS 5.0. The current version of Extrategies
is 6.0 and is included in PVS 6.0. Extrategies 6.0 is a significant revision of
the previous version. Extrategies 6.0 handles TCCs in a much cleaner
way and includes several new strategy combinators for writting strategies. It also
includes the proof command
deftactic for defining local strategies
(called tactics), whose scope is the branch of the proof where the
tactic is declared.
The strategies included in Extrategies 6.0 are:
The behavior of some strategies in Extrategies
6.0 may be slightly different from previous
versions. Because of this, some proofs that worked in PVS 5.0 may be broken in
PVS 6.0. In particular,
may generate formulas in a different order. In most cases, the old
skoletin can be simulated by setting the