On mechanical quantifier elimination for elementary algebra and geometry. (English) Zbl 0644.68051

Arnon, Dennis S.; Mignotte, Maurice

J. Symb. Comput. 5, No. 1-2, 237-259 (1988).

Summary: We give solutions to two problems of elementary algebra and geometry: (1) find conditions on real numbers p, q, and r so that the polynomial function \(f(x)=x\) \(4+px\) \(2+qx+r\) is nonnegative for all real x, and (2) find conditions on real numbers a, b, and c so that the ellipse (x-c) 2/a \(2+y\) 2/b \(2=1\) lies inside the unit circle y \(2+x\) \(2=1.\)
Our solutions are obtained by following the basic outline of the method of quantifier elimination by cylindrical algebraic decomposition [G. E. Collins, Lect. Notes Comput. Sci. 33, 134-183 (1975; Zbl 0318.02051)], but we have developed, and have been considerably aided by, modified versions 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 elimination problems of elementary algebra and geometry.

MSC:

68W30	Symbolic computation and algebraic computation
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
03C10	Quantifier elimination, model completeness, and related topics
03B35	Mechanization of proofs and logical operations
12D15	Fields related with sums of squares (formally real fields, Pythagorean fields, etc.)
14Pxx	Real algebraic and real-analytic geometry

Keywords:

quantifier elimination; cylindrical algebraic decomposition; elementary algebra; geometry

Citations:

Zbl 0318.02051

References:

[1]	Arnon, D. S., Algorithms for the Geometry of Semi-Algebraic Sets (1981), Comp. Sci. Dept., Univ.: Comp. Sci. Dept., Univ. Wisconsin-Madison, PhD thesis, Tech. Rept. #436
[2]	Arnon, D. S.; Smith, S., Towards a mechanical solution of the Kahan ellipse problem I, Proceedings of the European Computer Algebra Conference. Proceedings of the European Computer Algebra Conference, Springer Lec. Notes Comp. Sci, 162, 36-44 (1983) · Zbl 0553.68031
[3]	Arnon, D. S.; Collins, G. E.; McCallum, S., Cylindrical algebraic decomposition I: the basic algorithm, SIAM J. Comp., 13, 4, 865-877 (1984) · Zbl 0562.14001
[4]	Arnon, D. S., On mechanical quuantifier elimination For elementary algebra and geometry: automatic solution of a nontrivial problem, Proceedings of EUROCAL ’85. Proceedings of EUROCAL ’85, Springer Lec. Notes Comp. Sci, 204, 270-271 (1985)
[5]	Arnon, D. S., A cluster-based cylindrical algebraic decomposition algorithm, J. Symb. Comp., 5 (1988), (this issue) · Zbl 0648.68056
[6]	Arnon, D. S., Geometric reasoning with logic and algebra, Artificial Intelligence J. (1988), (special issue, on Geometric Reasoning and. Artificial Intelligence; to appear) · Zbl 0705.68086
[7]	Arnon, D. S.; Collins, G. E.; McCallum, S., An adjacency algorithm for cylindrical algebraic decompositions, or three-dimensional space, J. Symb. Comp., 5 (1988), (this issue) · Zbl 0648.68055
[8]	Collins, G. E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Proceedings of the Second GI Conference on Automata Theory and Formal Languages. Proceedings of the Second GI Conference on Automata Theory and Formal Languages, Springer Lec. Notes Comp. Sci, 33, 515-532 (1975)
[9]	Collins, G. E., SAC-2 and ALDES now available, ACM SIGSAM Bull, 14, 19 (1980)
[10]	Collins, G. E., Quantifier elimination for real closed fields: a guide to the literature, (Butchberger, B.; Loos, R.; Colllns, G. E., Computer Algebra - Symbolic and Algebraic Computation. Computer Algebra - Symbolic and Algebraic Computation, Computing Supplementum, 4 (1982), Springer-Verlag: Springer-Verlag Vienna and New York), 79-81 · Zbl 0495.03016
[11]	Collins, G. E.; Loos, R. G.K., Real zeros of polynomials, (Buchberger, B.; Logs, R.; Collins, G,E., Computer Algebra - Symbolic and Algebraic Computation. Computer Algebra - Symbolic and Algebraic Computation, Computing Supplementum, 4 (1982), Springer-Verlag: Springer-Verlag Vienna and New York), 83-94
[12]	Delzell, C., Private communication (1983)
[13]	Delzell, C., A continuous, constructlve solution to Hilbert’s 17th problem, Invent. math, 76, 365-384 (1984) · Zbl 0547.12017
[14]	Kahan, W., Problem No. 9: An ellipse problem, ACM SIGSAM Bull, 9, 35, 11 (1975)
[15]	Lauer, M., A solution to Kahan’s problem (SIGSAM problem no. 9), ACM SIGSAM Bull, 11, 16-28 (1977) · Zbl 0401.51010
[16]	Lazard, D., Quantifier elimination: optimal solution for two classical examples, J. Symb. Comp., 5 (1988), (this issue) · Zbl 0647.03023
[17]	McCallum, S., An improved projection operation for cylindrical algebraic decomposition of three-dimenslonal space, J. Symb. Comp., 5 (1988), (this issue)
[18]	Mignotte, M., Computer versus paper and pencil, Proc. CALSYF, 4, 63-69 (1986)
[19]	Tarski, A., A Decision Method for Elementary Algebra and Geometry, (Report R-109 (1951), The Rand Corporation: The Rand Corporation Santa Monica, CA) · Zbl 0044.25102