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

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.