Automatic Proving of Geometric Theorems

In this talk, we describe a system for automatic generation of binomial proofs for geometry theorems. Beginning with proofs in projective geometry, we show how Felix Klein’s adjunction principle permits extension of these binomial proof methods to Euclidean, and eventually to other, geometries. The present report for the conference proceedings is simply a ‘verbatim’ record of the talk, and will serve as an outline of material to appear in a subsequent publication by the same authors1. References to earlier work will be found in §25.