Basic principles of mechanical theorem proving in elementary geometries

Abstract

At the end of 1976 and the beginning of 1977, the author discovered a mechanical method for proving theorems in elementary geometries. This method can be applied to various unordered elementary geometries satisfying the Pascalian Axiom, or to theorems not involving the concept of ‘order’ (e.g., thatc is ‘between’a andb) in various elementary geometries. In Section 4 we give the detailed proofs of the basic principles underlying this method. In Sections 2 and 3 we present the theory of well-ordering of polynomials and a constructive theory of algebraic varieties. Our method is based on these theories, both of which are based on the work of J. F. Ritt. In Section 5 we use Morley's theorem and the Pascal-conic theorem discovered by the author to illustrate the computer implementation of the method.