什么是机器定理证明?

[拼音]：jiqi dingli zhengming

[外文]：mechanical theorem proving

把人证明数学定理和日常生活中的演绎推理变成一系列能在计算机上自动实现的符号演算的过程和技术，又称自动定理证明和自动演绎。机器定理证明是人工智能的重要研究领域，它的成果可应用于问题求解、自然语言理解、程序验证和自动程序设计等方面。数学定理证明的过程尽管每一步都很严格有据，但决定采取什么样的证明步骤，却依赖于经验、直觉、想象力和洞察力，需要人的智能。因此，数学定理的机器证明和其他类型的问题求解,就成为人工智能研究的起点。早在17世纪中叶，莱布尼兹就提出过用机器实现定理证明的思想。19世纪后期G.弗雷格的“思想语言”的形式系统，即后来的谓词演算，奠定了符号逻辑的基础，为自动演绎推理提供了必要的理论工具。20世纪50年代，由于数理逻辑的发展,特别是电子计算机的产生和应用,机器定理证明才变为现实。A.纽厄尔和H.A.西蒙首先用探试法实现了用以证明命题逻辑中重言式的逻辑理论家系统LT。后来，开始探讨通用的机器定理证明的方法，归结原理是其中突出的例子。

一阶谓词逻辑的恒真性问题是不可解的，即不存在能判定一阶逻辑中任意合式公式是不是恒真式的算法，但是这个问题又是部分可解的。如果A是恒真式,那么必有算法可以证明。许多一阶逻辑的证明算法都以J.厄尔布朗定理为基础，其中以1965年J.A.鲁宾逊提出的、对于一阶逻辑是完备的证明算法即归结原理最为著名。归结原理的提出，把机器定理证明的研究推向高潮。但归结原理不依赖于领域知识，不使用依赖问题领域的探试法，证明过程冗长，不能在合理的时间和计算机存储容量内证明较为复杂的数学定理，因此人们又提出非归结定理证明方法，后来又对以探试法为基础的问题求解技术发生兴趣。与此同时还出现了因否定归结原理进而否定所有自动演绎方法的倾向。但是人工智能所要解决的问题，其信息往往是不完全的，而且即使信息完全，要对有限的但为数众多的情形一一列举,实际上也不可行,因而只有用演绎推理的方法。逻辑程序设计和日本以PROLOG为原型开发第五代计算机系统的核语言，进一步恢复了归结原理和自动演绎技术的地位。人工智能的历史表明，以认知心理学为基础的探试法和以逻辑为基础的自动演绎相辅相成，不可偏废。自动演绎与探试法等技术相结合而不用归结原理的定理证明技术，主要用于数学定理的机器证明。

在数学定理机器证明中，有一类问题已有判定算法，如1951年W.斯米列夫给出的阿贝尔群判定算法，1951年A.塔斯基给出的初等几何和代数的判定算法，1960年王浩提出的命题逻辑判定算法和1976年以来吴文俊提出的初等几何和微分几何定理机器证明的理论和方法。

以经典的一阶逻辑为基础的自动演绎技术比较成熟。为了适应人工智能中复杂的推理形式，需要研究高阶逻辑和非标准逻辑中的自动演绎技术并从实用角度将这类逻辑表示形式转换成等价的经典一阶逻辑的表示形式。

将一阶谓词演算的子集直接作为程序设计语言的技术和方法。PROLOG语言是初步实现逻辑程序设计基本思想的第一个语言，R.科瓦尔斯基则曾对HORN子句作了过程性解释，系统地阐明了逻辑程序设计的基本理论。