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

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.