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

# 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 '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