** Next:** Some conventions and notation
** Up:** An Introduction to Quantifier
** Previous:** A short history of

Quantifier elimination by CAD consists of three phases: projection,
stack construction, and solution formula construction. Roughly
speaking, the projection phase produces an implicit representation of
a special kind of decomposition -- a cylindrical algebraic
decomposition -- of the space of 's variables and, with it, the
space of 's free variables. One important property of the
decomposition of free-variable space is that in any cell has the
same truth value at every point in the cell.
(The notion of the truth value of evaluated ``at a point'' is well
defined.
A point in free-variable space specifies a value for each free
variable in . Substituting those values for the free
variables leaves a sentence, which must be either true or false.)
The stack construction
phase builds an explicit representation of this decomposition, and
uses it to determine the truth of for each cell in the
decomposition of free-variable space. Finally, the solution formula
construction phase uses the decomposition of free-variable space to
construct , a quantifier-free formula equivalent to
.

**Subsections**

** Next:** Some conventions and notation
** Up:** An Introduction to Quantifier
** Previous:** A short history of
*Christopher W Brown*

*2001-07-10*