AUTOMATED PRODUCTION OF TRADITIONAL PROOFS FOR THEOREMS IN EUCLIDEAN GEOMETRY .1. THE HILBERT INTERSECTION POINT THEOREMS

We present a method which can produce traditional proofs for a class o f constructive geometry statements in Euclidean geometry. The method i s a mechanization of the traditional area method used by many geometer s. The key idea of our method is to eliminate dependent (constructed) points in a geometry statement using a few basic geometry propositions about the area of triangles. The method has been implemented. Our pro gram, called Euclid, can produce traditional proofs of many hard geome try theorems such as Pappus' theorem, Pascal's theorem, Gauss point th eorem, and the Pascal conic theorem. Currently, it has produced proofs of 110 nontrivial theorems entirely automatically. The proofs produce d by Euclid are elegant, short (often shorter than the proofs given by geometers) and understandable even to high school students. This meth od seems to be the first that can produce traditional proofs for hard geometry theorems automatically.