Quantifier Elimination for Formulas Constrained by Quadratic Equations via Slope Resultants
H. Hong · The Computer Journal · 1993
An algorithm is given for eliminating the quantifier from a formula: (∃x ∈ R)[a2x2 + a1x + a0 = 0 ∧ F], where F is a quantifier free formula in x1,…,xr, x, and a2, a1, a0 are polynomials in x1, …, xr with real coefficients such that the system {a2=0, a1=0, a0=0} has no solution in R;r. The output formulas are made of resultants and their variants, which we call slope resultants. The slope resultants can be, like the resultants, expressed as determinants of certain matrices. If we allow the determinant symbol in the output, the computing time of the algorithm is linear in the length of the input. If not, the computing time is dominated by N(n2r+1l+n2rl2) where N is the number of polynomials in the input formula, r is the number of variables, n is the maximum of the degrees for every variable, and l is the maximum of the integer coefficient bit lengths. Experiments with implementation suggest that the algorithm is sufficiently efficient to be useful in practice.