On the application of Buchberger's algorithm to automated geometry theorem proving

DOI10.1016/S0747-7171(86)80006-2zbMath0629.68086MaRDI QIDQ1094149

B. Kutzler, Sabine Stifter

Publication date: 1986

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

Gröbner basespolynomial equationsBuchberger's algorithmautomated geometry theorem proving

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Related Items (49)

Challenging theorem provers with Mathematical Olympiad problems in solid geometry ⋮ An extension of a procedure to prove statements in differential geometry ⋮ On the application of Buchberger's algorithm to automated geometry theorem proving ⋮ Using Gröbner bases to reason about geometry problems ⋮ Proof-checking Euclid ⋮ A bibliography of quantifier elimination for real closed fields ⋮ \textit{Theorema}: Towards computer-aided mathematical theory exploration ⋮ Computer-based manipulation of systems of equations in elasticity problems with Gröbner bases ⋮ Wu's method and its application to perspective viewing ⋮ Computing dimension and independent sets for polynomial ideals ⋮ Geometry theorem proving by decomposition of quasi-algebraic sets: An application of the Ritt-Wu principle ⋮ On the algebraic formulation of certain geometry statements and mechanical geometry theorem proving ⋮ A refutational approach to geometry theorem proving ⋮ Automated discovery of geometric theorems based on vector equations ⋮ Elimination procedures for mechanical theorem proving in geometry ⋮ The dimension method in elementary and differential geometry ⋮ A generalized Euclidean algorithm for geometry theorem proving ⋮ Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems ⋮ Mechanical theorem proving in projective geometry ⋮ Automatic deduction in (dynamic) geometry: Loci computation ⋮ Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method ⋮ 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 ⋮ Some reflections about the success and bibliographic impact of the dynamic geometry system \textit{GeoGebra} ⋮ Automated discovery of angle theorems ⋮ A program to create new geometry proof problems ⋮ Automated reducible geometric theorem proving and discovery by Gröbner basis method ⋮ What does ``without loss of generality mean, and how do we detect it ⋮ A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications ⋮ Gröbner bases and invariant theory ⋮ A procedure to prove statements in differential geometry ⋮ A review and prospect of readable machine proofs for geometry theorems ⋮ Cayley factorization and a straightening algorithm ⋮ Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry. ⋮ Multilinear Cayley factorization ⋮ On the synthetic factorization of projectively invariant polynomials ⋮ Invariant computations for analytic projective geometry ⋮ Some examples of the use of distances as coordinates for euclidean geometry ⋮ Computational algebraic geometry of projective configurations ⋮ Automated theorem proving practice with null geometric algebra ⋮ An introduction to geometry expert ⋮ A class of mechanically decidable problems beyond Tarski's model ⋮ A symbolic dynamic geometry system using the analytical geometry method ⋮ Connecting the 3D DGS Calques3D with the CAS Maple ⋮ Decomposing algebraic sets using Gröbner bases ⋮ Grassmann-Cayley algebra and robotics ⋮ Interfacing external CA systems for Gröbner bases computation in M<scp>izar</scp>proof checking ⋮ Geometric theorem proving by integrated logical and algebraic reasoning ⋮ Automated reasoning in differential geometry and mechanics using the characteristic set method. I: An improved version of Ritt-Wu's decomposition algorithm ⋮ Application of Gröbner bases to problems of movement of a particle

Cites Work

• On the application of Buchberger's algorithm to automated geometry theorem proving
• Using Gröbner bases to reason about geometry problems
• Proving geometry theorems with rewrite rules
• Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the application of Buchberger's algorithm to automated geometry theorem proving