复现50年前首个AI程序，成功证明16个数学定理
Executable Archaeology: Reanimating the Logic Theorist from its IPL-V Source
- 用Common Lisp重写IPL-V解释器，还原1963年版逻辑理论家代码
- 在《数学原理》第二章中成功证明16个定理，符合历史记录
- 首次时隔半世纪重新运行原始代码，适合人工智能史研究者
逻辑理论家（LT）由纽厄尔、肖和西蒙于1955-1956年创建，被广泛认为是首个人工智能程序。尽管其概念模型于1956年提出，但随着信息处理语言（IPL）的演进，该程序经历了多次迭代。本文构建了一个基于Common Lisp的IPL-V解释器，并从斯蒂费鲁德1963年兰德技术报告中直接转录的代码出发，忠实复现了逻辑理论家。斯蒂费鲁德版本是对原始启发式逻辑的规范化重构。复现后的LT成功证明了《数学原理》第二章中23个尝试定理中的16个，结果与原系统在搜索限制下的行为历史一致。据作者所知，这是自半个世纪以来首次成功执行原始逻辑理论家代码。
原文摘要 · Abstract (English)
The Logic Theorist (LT), created by Allen Newell, J. C. Shaw, and Herbert Simon in 1955-1956, is widely regarded as the first artificial intelligence program. While the original conceptual model was described in 1956, it underwent several iterations as the underlying Information Processing Language (IPL) evolved. Here I describe the construction of a new IPL-V interpreter, written in Common Lisp, and the faithful reanimation of the Logic Theorist from code transcribed directly from Stefferud's 1963 RAND technical report. Stefferud's version represents a pedagogical re-coding of the original heuristic logic into the standardized IPL-V. The reanimated LT successfully proves 16 of 23 attempted theorems from Chapter 2 of Principia Mathematica, results that are historically consistent with the original system's behavior within its search limits. To the author's knowledge, this is the first successful execution of the original Logic Theorist code in over half a century.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。