Partial Cylindrical Algebraic Decomposition for Quantifier Elimination

Cylindrical Algebraic Decomposition (CAD) by Collins (1975) provides a potentially powerful method for solution of many important mathematical problems by means of quantifier elimination, provided that the required amount of computation can be sufficiently reduced. Arnon (1981) introduced the important method of clustering for reducing the required computation and McCallum (1984) introduced an improved projection operation which is also very effective in reducing the amount of computation. In this paper we introduce yet another method for reducing the amount of computation which we will call partial CAD construction.