“所有符号派的人工智能技术的基础都是定理证明，如专家系统、知识表示和知识库。”

自动定理证明的研究某种意义上是继承了数学哲学三大派的逻辑主义和形式主义。逻辑论的源头是亚里士多德的三段论，现代逻辑的奠基人之一罗素认为“演绎逻辑里的所有事，机器都能干”。形式主义的代表人物希尔伯特主张数学就是把一串符号变成另一串符号。无论是逻辑论还是形式论，定理证明的过程就是一个归约的过程。自动证明就是研究这个数学过程的全自动化。以下是《人工智能简史》第二章的内容简介。

自动定理证明兴衰