定理证明是指数学领域中对臆测的定理寻求一个证明，证明定理时，不仅需要有根据假设进行演绎的能力，而且需要有某些知觉的技巧，这是一项需要智能才能完成的任务。

数学领域中对臆测的定理寻求一个证明，一直被认为是一项需要智能才能完成的任务。

证明定理时，不仅需要有根据假设进行演绎的能力，而且需要有某些知觉的技巧。例如数学家在求证一个定理时，会熟练地运用他丰富的专业知识，猜测应当先证明哪一个引理，精确判断出已有的那些定理将其作用，并把主问题分解为若干问题，分别独立进行求解。

因此人工智能研究中机器定理证明很早就受到注视。在人工智能的发展时期，1957年A.Newell、J.Shaw和H.Simon等人的心理学小组编制出一个称为逻辑理论机LT（The Logic Theory Machine）的数学定理证明程序，该程序证明了B.A.W.Russell和A.N.Whitehead的“数学原理”一书第二章的38个定理。并取得不少成果。

（1） 先想出大致的解题计划；

（2） 根据记忆中的公理定理和推理规则组织解题过程；

（3） 进行方法和目的分析，修正解题计划。

由此可见定理证明在人工智能的发展中已取得不少成果。

定理证明的研究在人工智能方法的发展中曾起到重要的作用，例如使用谓词逻辑语言，其演绎过程的形式体系研究，帮助人们更清楚地理解推理过程的各个组成部分。

许多其他领域的问题，如医疗诊断信息检索等也可以应用定理证明的方法，因此机器定理证明的研究具有普遍意义。