正文
几十年后，罗素和怀特海所著的《数学原理》已经将几乎所有的数学体系统一到一个“谓词逻辑”系统中了。整本书浸透了一种强烈依赖逻辑，而不依赖直觉的思维模式。这种思维模式在后世遭到了批判，比如说“1+1=2”这种生活中近乎直觉的思维结果，在《数学原理》中用了几十页才证毕。
20世纪2、30年代，一部分逻辑学家开始探讨机器证明这个问题，通俗讲，就是用机器证明数学定理。这些逻辑学家的目标就是找到一个判定逻辑真假的通用法则。这个通用法则一旦被找到，它就可以在被编程，由机器来执行，以判断数学命题。
后来，通用的法则被证明是可行的，Church消解定理被发现了。用机器（物理符号系统）证明数学定理就有了最基本的理论支持。后来的最广通代、m.g.u方法、Skolem范式都是基于此进行的。很多“泡面番”之类的文章将这些前人的工作几乎全部默认到了赫伯特·西蒙身上，仿佛他一夜之间就想出了机器证明的方法。
不过，平心而论，这些学者做的工作仅仅是在理论上证明可行性，那么数学课本上的定理真的可以被机器证明吗？给出答案的正是赫伯特·西蒙和他的合作者。
1956年夏举行的达特茅斯研讨会被后人公认为AI科学的肇端。会议的参与者里有两个耳熟能详的名字：香农（Shannon）皮茨（Pitts）。他们分别是计算机科学和人工神经网络学科的鼻祖中的鼻祖。
然而这两位只是负责围观的。不过大师就是大师，皮茨对于会议有很深入的总结，他敏锐地发现，这次研讨会出现了“两条路线”，一条是通过模拟人们的“里”（神经元活动方式）来达到模式识别，另外一条是通过模拟人们的“表”（思维活动方式）以让机器活动。然而这两条路线都没有拿出能够工作的“真家伙”来。前者只讲了一篇模式识别的文章，后者连文章都没有，以“空手接白刃”的精神讲怎么用计算机下棋。
然而皮茨没有察觉到的“第三条路线”却拿出了可以运行的“人工智能”。这个在当时唯一一个可用的人工智能程序就是西蒙和纽厄尔（A. Newell）的“逻辑理论家”（ Logic Theorist）。它能够证明《数学原理》一书中的“谓词演算”的38个定理（书中所有的“谓词演算”的350个定理全部被证明的工作由华人数学家王浩完成）。
“逻辑理论家”程序是在西蒙和同事一起开发的IPL（Information Processing Language）上编写和运行的，这是世界上第一个专门为人工智能开发设计的语言，也是第一个基于列表（List）的计算机语言。这一点弥足珍贵，要知道，IPL以前，计算机语言还仅仅是依附于“冯诺依曼结构”的编译和控制系统，而IPL使得计算机系统能够不受硬件限制,运行任何一种对应用来说是恰当的数据类型。
图3 最早于1957年运行FORTRAN编译器的IBM704型号计算机
有趣的是，西蒙在设计该语言的时候，用的是“人肉寄存器”——他让孩子们拿着牌子围绕周围，自己则在牌子上写变量。IPL语言一共有六个版本，发布了五代。基于IPL语言环境的人工智能程序还包括“通用问题求解”和“Compute Chess”。西蒙等人在“Compute Chess”的基础上，对于计算机如何通过“视觉”理解棋局和采用“复杂问题解决系统”下棋进行了一系列研究。
