**An Informal Description**

Informally, the quantifier elimination problem is this: Given a boolean combination of
equalities and inequalities of polynomials with integer coefficients in which some
variables appear quantified, produce an equivalent formula in
which no quantified variables appear (all variables are
assumed to be real).
For example, if the input formula is

**Quantifier Elimination Algorithms**

Quantifier elimination by CAD is one algorithm for QE. There
are others, and in the future this section will describe some of
them and point you to other systems for QE.

Christopher W Brown Last modified: Wed Jul 31 09:48:51 EDT 2002