An examination of the geometry theorem machine

Abstract

In five papers, Gelernter, Rochester, Hansen, and Loveland sketched in outline what they call a Geometry Theorem Machine and described results that were obtained when a computer was programmed to simulate the machine. More precisely, they described an algorithm for constructing proofs for theorems of an axiomatic theorý which is a portion of plane geometry. The papers are written in such a way that one can only conclude by inference details of the axiomatic theory and the algorithm for finding proofs for theorems in the theory. The purpose of this paper is to supply some of these details. © 1970.