1.4.1 自动定理证明

自动定理证明是用机器来帮助证明数学或逻辑中的一些结论是否正确。这是人工智能一个很重要的研究方向，也是让机器自我推理的关键技术。

自动定理证明的做法是把要证明的结论写成一种逻辑语言，然后让机器按照一些规则和步骤来找到证明或者反驳。

自动定理证明有两种主要方法：一种是完全交给机器去做，用到了SAT、SMT、一阶定理证明等算法；另一种是需要人和机器合作，人来提供一些提示和指导。

自动定理证明在很多领域都有用处，比如数学、计算机科学、软件工程、形式化方法等。它可以帮人们发现新的数学结论，检查已经证过的结论是否有错，保证程序和系统能正常和安全地运行等。

自动定理证明是人工智能里最早研究并成功应用的一个方向，也是推动人工智能发展的一个重要力量。其实，不光是数学里面的结论，像医疗诊断、信息检索、问题求解等很多其他领域的问题，也可以变成定理证明问题。

定理证明就是要证明从前提P出发能得到结论Q。但是，这样直接证明一般很难。常用的方法是反证。在这方面，海伯伦和鲁滨逊两位学者都做了很有价值的研究，提出了相应的理论和方法，为自动定理证明打下了理论基础。特别是鲁滨逊提出的归结原理让定理证明能在机器上实现，对机器推理有了重大贡献。我国吴文俊院士提出并实现的“吴氏方法”，可以让计算机证明几何定理，是机器定理证明领域的一项里程碑式成果。