An overview of quantifier elimination by CAD

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 $F$'s variables and, with it, the space of $F$'s free variables. One important property of the decomposition of free-variable space is that in any cell $F$ has the same truth value at every point in the cell. (The notion of the truth value of $F$ evaluated ``at a point'' is well defined. A point in free-variable space specifies a value for each free variable in $F$. 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 $F$ 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 ${\overline F}$, a quantifier-free formula equivalent to $F$.