Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry.
type: Item
instance of: scholarly article
title: Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry.
zbMATH Open document ID: 1047.03010
DOI: 10.1016/S0747-7171(03)00067-1
author: Yihong Wu
author: Hongbo Li
published in: Journal of Symbolic Computation
publication date: 2004-03-14T00:00:00Z
review text: An algorithm for proving geometric theorems of ruler-constructible type in two- and three- dimensional projective geometry is presented on the basis of some results on Cayley algebra and bracket algebra. In essence, the idea is to combine Cayley expansion and Cramer's rules with Cayley factorization and simplification techniques to get shorter proofs. For a geometric entity or constraint, there are often several different Cayley expressions to represent it which, in addition, usually have many ways to be expanded into bracket polynomials. Furthermore, the choice of an adequate representation can lead to extremely simple proofs whereas an unlucky choice can lead to extremely complicated computations. The central idea to overcome the difficulty of multiple representation, eliminations and expansions is to use what the authors call `breefs', that is, bracket-oriented representation, elimination and expansion for factored and shortest results. In this paper, the Cayley expansions of some typical Cayley expressions are given and a series of theorems are established on factored and shortest expansions; several Cayley factorization techniques are developed, which are also used in a companion paper on theorem proving in conic geometry [J. Symb. Comput. 36, No. 5, 763--809 (2003; Zbl 1047.03011), reviewed below] and from which a powerful simplification technique, called contraction, has been derived. Several elimination rules for theorem proving are obtained which, together with the Cayley expansion and simplification techniques, form the basis of the short-proof generation algorithm.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 51A05
Mathematics Subject Classification ID: 52B55
zbMATH DE Number: 2056563
zbMATH Keywords: automated theorem proving
zbMATH Keywords: incidence geometry
zbMATH Keywords: Cayley algebra
zbMATH Keywords: bracket algebra
zbMATH Keywords: projective geometry
MaRDI profile type: Publication
cites work: On the exterior calculus of invariant theory
cites work: On the finding of final polynomials
cites work: Computational synthetic geometry
cites work: Q3208084
cites work: Q3994509
cites work: Machine Proofs in Geometry
cites work: Automated production of traditional proofs in solid geometry
cites work: Q5690444
cites work: On the Foundations of Combinatorial Theory: IX Combinatorial Methods in Invariant Theory
cites work: Grassmann-Plücker relations and matroids with coefficients
cites work: Q4525303
cites work: Projective geometry with Clifford algebra
cites work: Q4299608
cites work: On the application of Buchberger's algorithm to automated geometry theorem proving
cites work: Vectorial equations solving for mechanical geometry theorem proving
cites work: Q4392227
cites work: Automated theorem proving in projective geometry with bracket algebra
cites work: Q4530836
cites work: Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry.
cites work: The dotted straightening algorithm
cites work: Mechanical theorem proving in projective geometry
cites work: Realization spaces of polytopes
cites work: Computing final polynomials and final syzygies using Buchberger's Gröbner bases method
cites work: Computational algebraic geometry of projective configurations
cites work: Algorithms in invariant theory
cites work: Gröbner bases and invariant theory
cites work: On the synthetic factorization of projectively invariant polynomials
cites work: Q4394960
cites work: The Bracket Ring of a Combinatorial Geometry. I
cites work: Multilinear Cayley factorization
cites work: Elimination methods
cites work: Invariant computations for analytic projective geometry
cites work: Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang
cites work: Q2716051
cites work: Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems
full work available at URL: s0747-7171(03)00067-1
OpenAlex ID: W4213292180
description: scientific article; zbMATH DE number 2056563