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.

• Examples
• Real Automation in the Field, César Muñoz and Micaela Mayero, Contractor Report ICASE, NASA/CR-2001-211271, 2001. BibTex Reference

The tag identifies links that are outside the NASA domain