Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry. (Q1426144)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry.
scientific article

    Statements

    Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry. (English)
    0 references
    0 references
    0 references
    14 March 2004
    0 references
    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.
    0 references
    automated theorem proving
    0 references
    conic geometry
    0 references
    Cayley algebra
    0 references
    bracket algebra
    0 references

    Identifiers