Andreas Seidl and Thomas Sturm: A Generic Projection Operator for
Partial Cylindrical Algebraic Decomposition

This paper provides a starting point for generic quantifier
elimination by partial cylindrical algebraic decomposition (PCAD). On
input of a first-order formula over the reals generic PCAD outputs a
theory and a quantifier-free formula. The theory is a set of negated
equations in the parameters of the input formula. The quantifier-free
formula is equivalent to the input for all parameter values satisfying
the theory. For obtaining this generic elimination procedure, we
derive a generic projection operator from the standard Collins--Hong
projection operator. Our operator particularly addresses formulas with
many parameters thus filling a gap in the applicability of PCAD. It
restricts decomposition to a reasonable subset of the entire space.
There is a theory in the form of negated equations generated that
describe this subset. The approach is compatible with other
improvements in the framework of PCAD. It turns out that the theory
contains assumptions that are easily interpretable and that are most
often non-degeneracy conditions. The applicability of our generic
elimination procedure significantly extends that of the corresponding
regular procedure. Our procedure is implemented in the computer logic
system REDLOG.