Improved projection for cylindrical algebraic decomposition

McCallum's projection operator for cylindrical algebraic decomposition (CAD ) represented a huge step forward for the practical utility of the CAD algo rithm. This paper presents a simple theorem showing that the mathematics in McCallum's paper actually point to a better projection operator than he pr oposes-a reduced McCallum projection. The reduced projection has the potent ial to not simply speed up CAD computation for problems that are currently solvable in practice, but actually increase the scope of problems that can realistically be attacked via CADs. Additionally, the same methods are used to show that McCallum's projection can be reduced still further when CAD i s applied to certain types of commonly occurring quantifier elimination pro blems. (C) 2001 Academic Press.