Quantifier elimination for formulas constrained by quadratic equations
Hoon Hong · 1993
An algorithm is given for constructing a quantifier free formula (a boolean expression of polynomial equations and inequalities) equivalent to a given formula of the form: (% c R)[azzz + alz + a. = O A F], where F is a quantifier free formula in Z1, . . . .z~, z, and az, al, ao are polynomials in z 1, . . . .Xr with real coefficients such that the system {az = O, al = O, a. = O} has no solution in Rr.Formulas of this form frequently occur in the context of constraint logic programming over the real numbers.The output formulas are made of resultants and two variants, which we call trace and slope resultants.Both of these variant resultants can be expressed as determinants of certain matrices.Problem In this section, we give an exact statement of the problem which will be tackled in the next section.First we introduce a few definitions in order to facilitate the subsequent discussions.Definition 1 (Atomic formula) An atomic formula in xl,..., XT is one of the forms: A = O, A # O, A >0, A <0, A ~O, and A ~O, where A is a polynomial in Il@l,.... z].].