Empirical Explorations of the Geometry Theorem Machine

Herbert Gelernter, J. R. Hansen and D. W. Loveland published a conference paper documenting empirical work with an IBM 704 geometry theorem-proving machine. The paper reports that the system had proved its first elementary Euclidean plane-geometry theorem in early spring 1959 and subsequently solved numerous textbook and examination problems.