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

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


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
Full Text: DOI


[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
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.