# zbMATH — the first resource for mathematics

Partial cylindrical algebraic decomposition for quantifier elimination. (English) Zbl 0754.68063
From the authors’ abstract: “The Cylindrical Algebraic Decomposition method (CAD) decomposes $$R^ n$$ 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”.

##### MSC:
 68W30 Symbolic computation and algebraic computation