SIMPLIFICATION OF QUANTIFIER-FREE FORMULAS 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 is simpler. The notion of a formula being simpler will be specified. An o verview is given over various methods combining elements of field theo ry, order theory, and logic. These methods do not require a Boolean no rmal form computation. They have been developed and implemented in RED UCE for simplifying intermediate and final results of automatic quanti fier elimination by elimination sets. Their applicability is certainly not restricted to the area of quantifier elimination. (C) 1997 Academ ic Press Limited.