NASA logo

+ Contact NASA

  • + HOME
  • + TEAM
  • + LINKS

  • Field

    Field is a set of PVS* strategies for simplifications and algebraic manipulations in the closed field of real numbers. The main strategy in the package is called field and it was originally based on a Coq tactic developed by Mayero and Delahaye. The strategy first removes the inverses that occur in a relational formula and then applies PVS decision procedures.

    Field has been part of PVS since PVS 5.0 and is included in the latest release of PVS*. The strategies included in Field are: field, grind-reals, real-props, neg-formula, add-formulas, sub-formulas, cancel-by, cancel-formula, both-sides-f, and sq-simp. This list is printed by the proof command field-about.

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