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.
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 language | English |
---|---|
Title of host publication | Proceedings SC2 2019 |
Number of pages | 8 |
Publication status | Published - Sept 2019 |