On mechanical quantifier elimination for elementary algebra and geometry

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)

zbMATH Keywords

geometryquantifier eliminationcylindrical algebraic decompositionelementary algebra

Mathematics Subject Classification ID

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 (13)

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

This page was built for publication: On mechanical quantifier elimination for elementary algebra and geometry