Simplification of Quantifier-free Formulae over Ordered Fields

Given a quantifier-free first-order formula over the theory of ordered fields, our aim is to find an equivalent first-order formula that issimpler. The notion of a formula being simpler will be specified. An overview is given over various methods combining elements of field theory, order theory, and logic. These methods do not require a Boolean normal form computation. They have been developed and implemented in for simplifying intermediate and final results of automatic quantifier elimination by elimination sets. Their applicability is certainly not restricted to the area of quantifier elimination.