逻辑理论家在达特茅斯夏季会议上展示

背景

1955年8月31日的一份提案，为一次夏季研究项目定下了计划，项目研究的对象在提案里被直接命名。提案提议在1956年夏天，于新罕布什尔州汉诺威的达特茅斯学院（Dartmouth College）进行为期2个月、10人规模的人工智能（artificial intelligence）研究^[2]。署名的是4个人：达特茅斯学院的J. 麦卡锡（John McCarthy）、哈佛大学的M. L. 明斯基（Marvin Minsky）、IBM公司的N. 罗切斯特（Nathan Rochester）和贝尔电话实验室的C. E. 香农（Claude Shannon）^[2]。提案的核心是一个猜想：学习以及智能的其他任何特征，原则上都可以被精确地描述，精确到足以造出一台机器来模拟它^[2]。提案请求洛克菲勒基金会（Rockefeller Foundation）提供资助，列出的总预算为13,500美元^[2]。「人工智能」这个词，一般认为是麦卡锡为了这次会议、在这份提案里提出来的^[1]。

这个猜想的落点在「描述」而不在「机器」，值得慢慢读。它并没有断定某一台机器一定会被造出来，而是说，只要一种心智能力能够被精确地说清楚，那么造一台能再现它的机器，在原则上就是可能的。由此而来的研究纲领也就分成两半：先说清楚某一部分智能究竟是什么，再让它跑起来。

会议

会议在1956年夏天举行，组织者正是麦卡锡、明斯基、香农和罗切斯特4人^[1]。会上展示的内容之一，是纽厄尔（Newell）与西蒙（Simon）的「逻辑理论家」（Logic Theorist）程序^[1]。

程序做了什么

「逻辑理论家」工作的领域是《数学原理》（Principia Mathematica）——一部讨论数学基础的书，它把书里的定理当作自己的题目。在形式系统里证明一条定理，本质上是一次搜索：从公理和推理规则出发，一步一步往下推，直到想要的那个命题作为推导中的一行出现。因为每一步都由规则许可，整个过程完全可以交给一个只摆弄符号、并不理解符号含义的东西去做，这正是它适合机器的原因。

到在达特茅斯展示的时候，这个程序已经证明了《数学原理》第2章前52条定理中的38条^[1]。它还给出了定理2.85的一个更短的证明，这个证明被拿给伯特兰·罗素（Bertrand Russell）看了^[1]。对读过这本书的人来说，后一个结果更出乎意料：找到证明是一回事，找到比书里印着的那个更好的证明是另一回事。