Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry.

DOI10.1016/S0747-7171(03)00067-1zbMath1047.03010OpenAlexW4213292180MaRDI QIDQ1426143

Yihong Wu, Hong-Bo Li

Publication date: 14 March 2004

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

Full work available at URL: https://doi.org/10.1016/s0747-7171(03)00067-1

zbMATH Keywords

projective geometryincidence geometryautomated theorem provingCayley algebrabracket algebra

Mathematics Subject Classification ID

Computational aspects related to convexity (52B55) Mechanization of proofs and logical operations (03B35) General theory of linear incidence geometry and projective geometries (51A05)

Related Items

Two cryptomorphic formalizations of projective incidence geometry ⋮ Collision and intersection detection of two ruled surfaces using bracket method ⋮ Body-and-cad geometric constraint systems ⋮ Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry. ⋮ Affine bracket algebra theory and algorithms and their applications in mechanical theorem proving ⋮ Cayley factorization and the area principle ⋮ Implementing geometric algebra products with binary trees ⋮ A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry

Cites Work

• On the finding of final polynomials
• The dotted straightening algorithm
• Gröbner bases and invariant theory
• On the exterior calculus of invariant theory
• On the application of Buchberger's algorithm to automated geometry theorem proving
• Elimination methods
• Projective geometry with Clifford algebra
• Multilinear Cayley factorization
• On the synthetic factorization of projectively invariant polynomials
• Invariant computations for analytic projective geometry
• Computational algebraic geometry of projective configurations
• Computational synthetic geometry
• Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang
• Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry.
• Vectorial equations solving for mechanical geometry theorem proving
• Grassmann-Plücker relations and matroids with coefficients
• Automated production of traditional proofs in solid geometry
• Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems
• Mechanical theorem proving in projective geometry
• Realization spaces of polytopes
• Computing final polynomials and final syzygies using Buchberger's Gröbner bases method
• On the Foundations of Combinatorial Theory: IX Combinatorial Methods in Invariant Theory
• The Bracket Ring of a Combinatorial Geometry. I
• Machine Proofs in Geometry
• Algorithms in invariant theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item