1.4.1 自动定理证明

自动定理证明是最早进行研究并得到成功应用的一个人工智能研究领域，对人工智能的发展起到了重要的推动作用。实际上，除数学定理证明以外，医疗诊断、信息检索、问题求解等许多非数学领域的问题，都可以被转化为定理证明问题。

定理证明的实质是证明由前提P得到结论Q的永真性。但是，要直接证明P→Q的永真性一般来说是很困难的，通常采用的方法是反证法。在这方面，法国巴黎高等师范学院数学博士雅克·埃尔布朗（Jacques Herbrand）与鲁滨逊先后进行了卓有成效的研究，提出了相应的理论及方法，为自动定理证明奠定了理论基础。尤其是鲁滨逊提出的归结原理使定理证明得以在计算机上实现，对机器推理做出了重要贡献。我国吴文俊院士提出并实现的几何定理机器证明“吴氏方法”，是机器定理证明领域的一项标志性成果。