On mechanical quantifier elimination for elementary algebra and geometry
From MaRDI portal
Publication:1102744
DOI10.1016/S0747-7171(88)80014-2zbMath0644.68051MaRDI QIDQ1102744
Dennis S. Arnon, Maurice Mignotte
Publication date: 1988
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Symbolic computation and algebraic computation (68W30) Fields related with sums of squares (formally real fields, Pythagorean fields, etc.) (12D15) Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10) Real algebraic and real-analytic geometry (14Pxx)
Related Items
On maps which preserve semipositivity and quantifier elimination theory for real numbers, A bibliography of quantifier elimination for real closed fields, A cluster-based cylindrical algebraic decomposition algorithm, Résolution du problème de l'ellipse et du cercle par l'algorithme de Hörmander, Visually dynamic presentation of proofs in plane geometry. II: Automated generation of visually dynamic presentations with the full-angle method and the deductive database method, Quantifier elimination theory and maps which preserve semipositivity, Geometric reasoning with logic and algebra, Partial cylindrical algebraic decomposition for quantifier elimination, An algorithm for solving parametric linear systems, A Simple Quantifier-Free Formula of Positive Semidefinite Cyclic Ternary Quartic Forms, Recent advances on determining the number of real roots of parametric polynomials, Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition, Computation of equilibria in noncooperative games
Cites Work
- A continuous, constructive solution to Hilbert's \(17^{th}\) problem
- Geometric reasoning with logic and algebra
- Quantifier elimination: Optimal solution for two classical examples
- An adjacency algorithm for cylindrical algebraic decompositions of three- dimensional space
- A cluster-based cylindrical algebraic decomposition algorithm
- A solution to Kahan's problem (SIGSAM problem no. 9)
- Cylindrical Algebraic Decomposition I: The Basic Algorithm
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
