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
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:
sq-simp. This list is printed by the proof command