机器定理证明是人工智能的重要研究领域，它的成果可应用于
问题求解、
自然语言理解、
程序验证和自动程序设计等方面。数学
定理证明的过程尽管每一步都很严格有据，但决定采取什么样的证明步骤，却依赖于经验、直觉、想象力和洞察力，需要人的智能。因此，数学定理的
机器证明和其他类型的问题求解,就成为人工智能研究的起点。早在17世纪中叶，
莱布尼兹就提出过用机器实现定理证明的思想。19世纪后期G.
弗雷格的“思想语言”的
形式系统，即后来的
谓词演算，奠定了
符号逻辑的基础，为自动
演绎推理提供了必要的理论工具。20世纪50年代，由于
数理逻辑的发展,特别是电子计算机的产生和应用,机器定理证明才变为现实。A.纽厄尔和H.A.西蒙首先用探试法实现了用以证明
命题逻辑中
重言式的逻辑理论家系统LT。后来，开始探讨通用的机器定理证明的方法，
归结原理是其中突出的例子。
归结原理和
非归结定理证明一阶
谓词逻辑的恒真性问题是不可解的，即不存在能判定
一阶逻辑中任意
合式公式是不是恒真式的算法，但是这个问题又是部分可解的。如果A是恒真式,那么必有算法可以证明。许多一阶逻辑的证明算法都以J.厄尔
布朗定理为基础，其中以1965年J.A.鲁宾逊提出的、对于一阶逻辑是完备的证明算法即归结原理最为著名。归结原理的提出，把机器定理证明的研究推向高潮。但归结原理不依赖于领域知识，不使用依赖问题领域的探试法，证明过程冗长，不能在合理的时间和计算机
存储容量内证明较为复杂的数学定理，因此人们又提出
非归结定理证明方法，后来又对以探试法为基础的
问题求解技术发生兴趣。与此同时还出现了因否定
归结原理进而否定所有
自动演绎方法的倾向。但是人工智能所要解决的问题，其信息往往是不完全的，而且即使信息完全，要对有限的但为数众多的情形一一列举,实际上也不可行,因而只有用
演绎推理的方法。
逻辑程序设计和日本以
PROLOG为原型开发第五代计算机系统的核语言，进一步恢复了归结原理和自动演绎技术的地位。人工智能的历史表明，以
认知心理学为基础的探试法和以逻辑为基础的自动演绎相辅相成，不可偏废。自动演绎与探试法等技术相结合而不用归结原理的
定理证明技术，主要用于数学定理的
机器证明。
几何定理的机器证明在数学
定理机器证明中，有一类问题已有判定算法，如1951年W.斯米列夫给出的
阿贝尔群判定算法，1951年A.塔斯基给出的初等几何和代数的判定算法，1960年王浩提出的
命题逻辑判定算法和1976年以来吴文俊提出的初等几何和
微分几何定理机器证明的理论和方法。
非标准逻辑中的自动演绎以经典的
一阶逻辑为基础的
自动演绎技术比较成熟。为了适应人工智能中复杂的推理形式，需要研究
高阶逻辑和非标准逻辑中的自动演绎技术并从实用角度将这类
逻辑表示形式转换成等价的经典一阶逻辑的表示形式。
逻辑程序设计将一阶
谓词演算的子集直接作为程序设计语言的技术和方法。
PROLOG语言是初步实现逻辑程序设计基本思想的第一个语言，R.科瓦尔斯基则曾对HORN子句作了过程性解释，系统地阐明了逻辑程序设计的基本理论。