Quantifier elimination for real algebra---the cubic case
Volker Weispfenning · 1994
We present a special purpose quantifier elimination method that eliminates a quantifier ∃x in formulas ∃x(4) where 4 is a boolean combination of polynomial inequalities of degree ≤3 with respect to x. The method extends the virtual substitution of parametrized test points developed in [Weispfenning 1, Loos &. We ispf.] for the linear case and in [Weispfenning2] for the quadratic case. It has similar upper complexity bounds and offers similar advantages (relatively large preprocessing part, explicit parametric solutions). small examples suggest that the method will be of practical significance.