Quantifier elimination: Optimal solution for two classical examples. (English) Zbl 0647.03023

Lazard, Daniel

J. Symb. Comput. 5, No. 1-2, 261-266 (1988).

Two equivalent quantifier-free formulas corresponding to the following two problems are given: \((1)\quad (\forall x)P(x)\geq 0,\) where P(x) is a polynomial of degree 4, \((2)\quad (\forall x)(\forall y)E(x,y)=0\Rightarrow C(x,y)\leq 0,\) where E(x,y) and C(x,y) are the ellipse and, respectively, unit circle expressions. The solutions are elegant and need elementary calculus.

Reviewer: D.Lucanu

MSC:

03C10	Quantifier elimination, model completeness, and related topics
68W30	Symbolic computation and algebraic computation
03D15	Complexity of computation (including implicit computational complexity)
68Q25	Analysis of algorithms and problem complexity

Keywords:

quantifier elimination; positive polynomial problem; ellipse problem

References:

[1]	Arnon, D. S., On mechanical quantifier elimination for elemenlary algebra and geometry: solution of a non-trivial problem, EUROCAL 85. Springer Lec. Notes Comp, Sci., 204, 270-271 (1985)
[2]	Arnon, D. S.; Smith, S,F., Toward mechanical solution of the Kahan ellipse problem l, EUROCAL 83. Springer Lec. Notes Comp. Sci., 162, 36-44 (1983)
[3]	Kahan, W., Problem #9: An ellipse problem, SIGSAM Bull. ACM, 9, 11 (1975)
[4]	Lauer, M., A solution to Kahan’s problem (SIGSAM problem no. 9), SIGSAM Bull. ACM, II, 16-20 (1977) · Zbl 0401.51010
[5]	Mignotte, M., Computer versus paper and pencil (1985), (CALSYF no. 4.)
[6]	Weiss, E., Algebraic Number Theory (1963), McGraw-Hill: McGraw-Hill New York