<p>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.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Geometry machine revisited

  • Predrag Janičić,
  • Julien Narboux

摘要

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.