References:
人工智能是一门新学科，历史的读物并不多。波登的《认知科学历史》（Boden 2008）和尼尔森的 《人工智能探究》（Nilsson 2010）是两本严肃的读物。 Nilson是人工智能学科的早期参与者，也一直是领导者之一，他多年担任SRI的人工智能部门负责人和 斯坦福大学计算机主任。
Pamela McCorduck, 1979 <能思考的机器>（Machines Who Think），取材立意都略微过时。
雅各布森（Annie Jacobsen）的《五角大楼大脑》(Pentagon’s Brain)是关于ARPA的详实而有趣 的历史。从这本书中我们可以看到信息科技一直不是ARPA的主打方向，但互联网这个ARPA歪打正着的项目 却是它最好的投资。
数学哲学有三大派：逻辑主义、形式主义、直觉主义。
逻辑主义的代表人物是罗素，主旨是把数学归约到逻辑，这样只要把逻辑问题解决了，之上的数学问题自然 就解决了。也就是说，把逻辑玩转了，数学就不算事儿。
希尔伯特主导的形式主义是另一派，他的梦想是把数学形式化，数学过程就是把一串符号变成另一串符号。 希尔伯特设想，如果能设计一个大一统的算法，那么所有的数学问题都可以由这个算法来解答。这和逻辑主义 精神有一定想通之处。哥德尔后来证明这一切是不可能的。
机器定理证明的研究从某种意义上继承了罗素和希尔伯特的思想：用机器来证明和判定那些可以证明和判定 的问题。纽厄尔和司马贺的“逻辑理论家”就是早期的机器定理证明程序，他们曾经给罗素写信，期盼能得到 伟人的首肯，罗素在回信时说：“我相信演绎逻辑里的所有事，机器都能干”。
人工智能中符号派的思想源头和理论基础就是定理证明，不懂定理证明就没法深入了解符号派。 戴维斯（Martin Davis，1928 –）1954年完成了第一个定理证明程序，所用的机器是普林斯顿高等研究院的一台 以冯诺依曼昵称“强尼”（Johnie）命名的电子管计算机“大强尼”（JOHNNIAC），而文章则迟至1957年才 公开发表。
戴维斯(1928 – )是富有成就的数学家和逻辑学家。戴维斯家境不好，大学时上了被称为“穷人哈佛”的 纽约市立学院（CCNY）– 那学校不收学费。在那儿他遇见了坡斯特（Emil Post）。 在1957年写的教科书《可计算性和不可解性》最早系统地介绍了坡斯特（Emil Post） 的工作，外界才开始得知坡斯特的名字。戴维斯最重要的贡献是和哲学家普特南（Hilary Putnam）等人 解决了希尔伯特第十问题。机器定理证明是他一直感兴趣的副业。
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?