Abstract

There are two relevant methods for CAD: McCallum [1984] which used order invariant CAD's and Lazard [Lazard1994, McCallumetal2019] which used lex-least invariant CADs, and doesn't have the nullification problem of McCallum [1984]. McCallum [1999] was the first to prove a CAD operator based on McCallum [1984], that took advantage of an equational constraint.
In this paper, we do the same for Lazard's method. This takes in a lex-least invariant CAD of $\RR^{n-1}$ as input and outputs a sign invariant CAD of $\RR^n$: consequently, it cannot be used recursively, but only for $x_n$, the first variable to be projected. In the further steps of the projection phase, we use Lazard's original projection operator. Nonetheless, reducing the output in the first step has a domino effect throughout the remaining steps, which significantly reduces the complexity. The long-term goal is to find a general projection operator that takes advantage of the equality constraint and can be used recursively, and this operator gives an important first step in that direction.
Original languageEnglish
Title of host publicationProceedings SC2 2019
Number of pages8
Publication statusPublished - Sep 2019

Cite this