On the application of Buchberger's algorithm to automated geometry theorem proving
From MaRDI portal
Publication:1094149
DOI10.1016/S0747-7171(86)80006-2zbMath0629.68086MaRDI QIDQ1094149
Publication date: 1986
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Related Items
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
