NASA logo

+ Contact NASA

  • + HOME
  • + TEAM
  • + LINKS

  • Extrategies

    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: