Because of the recursive nature of CAD's, the natural algebraic decomposition defined by is a CAD of -- the induced CAD of -space. Since (the set of polynomials appearing in ) is contained in , the induced CAD of -space (the space of the free variables of ) is truth-invariant with respect to . This means that for any two points and in the same cell, . The truth invariance of the induced CAD of -space is crucial for the application of CAD's to quantifier elimination.
The to be computed by the projection phase is not unique, and there have been several ``projection operators'' proposed for the construction of [Collins(1975),Hong(1990),McCallum(1998),Brown(2001)]. A projection operator, , is a function that maps a set of -level polynomials to a set of polynomials of level less than . Let be a set of -level polynomials, and let be . The key property of is that if is a region in in which the elements of have invariant sign, then the maximal sign-invariant regions of form a stack in . A set of polynomials that is closed under the projection operator is easily seen to define a CAD -- i.e. the natural algebraic decomposition of such a set is a CAD. The set of projection factors is constructed by computing the irreducible factors of the -closure of the set of polynomials appearing in . It is sufficient to deal with these irreducible factors and much more efficient.