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

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.

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 |

### Citations:

Zbl 0318.02051
PDF
BibTeX
XML
Cite

\textit{D. S. Arnon} and \textit{M. Mignotte}, J. Symb. Comput. 5, No. 1--2, 237--259 (1988; Zbl 0644.68051)

Full Text:
DOI

### 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 |

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.