** Next:** Stack construction
** Up:** An overview of quantifier
** Previous:** What is a CAD?

##

Projection

Any set of polynomials in
defines a * natural
algebraic decomposition* of into maximal connected regions in
which the elements of the set have invariant signs. Let be the set of
polynomials appearing in . The goal of the projection phase is to
produce a set ,
, such
that the natural decomposition defined by is a CAD. The set
is called a * projection factor set*.
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.

** Next:** Stack construction
** Up:** An overview of quantifier
** Previous:** What is a CAD?
*Christopher W Brown*

*2001-07-10*