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 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 REDUCE 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.