逻辑理论家（Logic Theorist）

这是什么

逻辑理论家（Logic Theorist）是 Allen Newell、Herbert A. Simon 与 Cliff Shaw 在 1956 年完成的一个计算机程序^[1]。它做的事情是自动推理：把用 Whitehead 与 Bertrand Russell《数学原理》（Principia Mathematica）符号写成的定理交给机器，由程序自己找出一条能够证明该定理的逻辑步骤链。它被描述为第一个有意为自动推理而设计的程序，也被称为「第一个人工智能程序」^[1]。

由来

1955 年，Newell 和 Simon 开始这项工作，当时人工智能这个领域还不存在^[1]。第一个版本是用手工模拟运行的：程序被写在 3x5 英寸的卡片上，1956 年 1 月，一个小组成员每人拿到一张卡片，其中就有 Simon 的妻子和三个孩子^[1]。后来 Cliff Shaw 在 RAND 圣莫尼卡设施的计算机上真正运行了这个程序^[1]。这项工作写成《The Logic Theory Machine: A Complex Information Processing System》，RAND 自己的文献目录把它列为 1956 年 7 月的 RAND Paper P-868^[3]。

它引入的几个概念

Computer History Museum 认为，逻辑理论家给人工智能带来了几个关键概念：启发式（heuristics）、表处理（list processing），以及把推理看作搜索（reasoning as search）^[2]。启发式是不保证最优、但能大幅缩小尝试范围的经验规则；比如下棋程序不去穷举所有合法着法，只看少数几种看起来有希望的走法，靠的就是启发式。表处理指把信息组织成可以随时增删的列表，而不是塞进一块固定的数字里。把推理看作搜索，则是把「证明一个定理」当成在一个状态空间里移动：从待证的命题出发，一步步走向公理和已有结论。这几个说法为后来的研究提供了描述推理程序在做什么的词汇。

结果

它证明了《数学原理》第二章前 52 个定理中的 38 个^[1]。对定理 2.85，它找到了一条新的、更短的证明，这条证明被认为比 Russell 和 Whitehead 手写的证明更优雅^[1]。Simon 把这条新证明拿给 Russell 本人看，据说 Russell 的反应是高兴^[1]。但把这条新证明投给《The Journal of Symbolic Logic》时被拒，理由是给一个初等定理找出新证明算不上什么贡献^[1]。

反响

1956 年夏天，Newell 和 Simon 在由 John McCarthy、Marvin Minsky、Claude Shannon 与 Nathan Rochester 组织的会议上报告了逻辑理论家，现场反应并不热烈^[1]。Computer History Museum 的时间线也记下了这个项目，说 Newell、Simon 与 J.C. Shaw 开始做的是一个最终会证明《数学原理》中 38 个定理的程序^[2]。

在发展中的位置

逻辑理论家出现在人工智能还没有定名、也还没有形成研究群体的年代：程序先于领域出现，而后来用来描述这类工作的词汇——启发式、表处理、推理即搜索——有一部分正来自它^[1][2]。它证明了机器可以做成一件通常被认为需要数学家判断力的事；而那次被期刊退稿的经历也说明，在当时看来，这更像一桩小小的趣闻，而不是对逻辑学的贡献^[1]。