McCallum improved the original Collins CAD projection operator (assuming well-orientation) and reduced the projection set even further for quantifier elimination problems which have equality constraints [6, 7]. Lazard provided a projection operator (and corresponding lifting process) that reduces the projection set as compared to McCallum's and is unconditional like Collins' original algorithm . Our research extends Lazard's work by providing a modification that reduces the projection set even further when there is a single equality constraint in the quantifier elimination problem (as in ). We also report a slight error in .
ASJC Scopus subject areas
- Computational Theory and Mathematics
- Computational Mathematics