Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry.
type: Item
instance of: scholarly article
title: Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry.
zbMATH Open document ID: 1047.03011
DOI: 10.1016/S0747-7171(03)00066-X
author: Yihong Wu
author: Hongbo Li
published in: Journal of Symbolic Computation
publication date: 2004-03-14T00:00:00Z
review text: This paper is a continuation of Part I [J. Symb. Comput. 36, No. 5, 717--762 (2003; Zbl 1047.03010), reviewed above] in which the focus is on proving theorems in plane conic geometry; this field is usually harder than incidence geometry from the standpoint of proof mechanization. The idea of bracket computation stated in Part I is developed now for plane conic geometry, the main algorithm being a conic points selection which selects, to a given construction, a suitable sequence of representative conic points for each bracket or wedge product containing the construction. The study of the particular construction of six-point-on-conic leads to the idea of considering its algebraic representations as computation rules. As a result, three additional simplification techniques are presented in this paper; namely, conic transformation, pseudoconic transformation and conic contraction. The additional concept of rational Cayley factorization is included in this paper; it allows the occurrence of bracket monomials in the denominator (hence the name). Technically, it is just a combination of the Cayley factorization techniques from Part I and the conic combination technique; from the computational side, it allows the authors to significantly simplify bracket computation in conic geometry. An automated theorem proving algorithm is presented at the end of the paper together with some sample applications of some theorems on free conic points, tangents and poles related to tangents.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 52B55
zbMATH DE Number: 2056564
zbMATH Keywords: automated theorem proving
zbMATH Keywords: conic geometry
zbMATH Keywords: Cayley algebra
zbMATH Keywords: bracket algebra
MaRDI profile type: Publication
cites work: On the exterior calculus of invariant theory
cites work: Geometry. I, II. Transl. from the French by M. Cole and S. Levy
cites work: Q4398782
cites work: Computational synthetic geometry
cites work: Q3208084
cites work: Q3994509
cites work: Machine Proofs in Geometry
cites work: Q5690444
cites work: On the Foundations of Combinatorial Theory: IX Combinatorial Methods in Invariant Theory
cites work: Q4525303
cites work: Some examples of the use of distances as coordinates for euclidean geometry
cites work: Projective geometry with Clifford algebra
cites work: Q4299608
cites work: Q4862317
cites work: Automated theorem proving in projective geometry with bracket algebra
cites work: Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry.
cites work: Q5732257
cites work: Mechanical theorem proving in projective geometry
cites work: Realization spaces of polytopes
cites work: Q5811706
cites work: Computational algebraic geometry of projective configurations
cites work: Algorithms in invariant theory
cites work: On the synthetic factorization of projectively invariant polynomials
cites work: Elimination methods
cites work: The Bracket Ring of a Combinatorial Geometry. I
cites work: Multilinear Cayley factorization
cites work: Q2716051
Recommended article: Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry.
Recommended article: Automated Deduction in Geometry
Recommended article: Q4530836
Recommended article: Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems
Recommended article: Q3700869
Recommended article: Wu's method and its application to perspective viewing
Recommended article: Q4234209
Recommended article: Q3700871
Recommended article: Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles
description: scientific article; zbMATH DE number 2056564