Geometry machine revisited
摘要
Gelernter’s Geometry Machine is significant not only as the pioneering automated prover for geometry but also as one of the earliest successful artificial intelligence systems. Although developed nearly seventy years ago, this seminal work in some aspects still remains fresh and inspiring. In this paper, we provide historical reflections on the Geometry Machine and its successors, and also utilize modern reasoning tools and full automation to reproduce, illustrate, and verify its results. That work leads to a framework that elevates the pre-1990s synthetic geometry theorem proving to a substantially higher level, providing robust support for other, more complex geometric axiomatic systems.