Partial Cylindrical Algebraic Decomposition for quantifier elimination

The Cylindrical Algebraic Decomposition method (CAD) decomposes Rr into regions over which given polynomials have constant signs. An important application of CAD is quantifier elimination in elementary algebra and geometry. In this paper we present a method which intermingles CAD construction with truth evaluation so that parts of the CAD are constructed only as needed to further truth evaluation and aborts CAD construction as soon as no more truth evaluation is needed. The truth evaluation utilizes in an essential way any quantifiers which are present and additionally takes account of atomic formulas from which some variables are absent. Preliminary observations show that the new method is always more efficient than the original, and often significantly more efficient