On mechanical quantifier elimination for elementary algebra and geometry

We give solutions to two problems of elementary algebra and geometry: (1) find conditlons on real numbers p, q, and r; so that the polynomial function f(x) = x4 + px2 + q x+ r is nonnegative for all real x and (2) find conditions on real numbers a, b, and c so that the ellipse (x−c)2q2+y2b2−1=0 lies inside the unit circle y2 + x2 - 1 = O. Our solutions are obtained by following the basic outline of the method of quantifier elimination by cylindrical algebraic decomposition (Collins, 1975), but we have developed, and have been considerably aided by, modified vcrsions of certain of its steps. We have found three equally simple but not obviously equivalent solutions for the first problem, illustrating the difficulty of obtaining unique “simplest” solutions to quantifier eliminetion problems of elementary algebra and geometry