机器定理证明

机器定理证明是一种将人类证明数学定理和日常生活中演绎推理转化为可在计算机上自动执行的符号运算的过程和技术。这一领域也被称为自动定理证明或自动演绎^[1][2][3]。

机器定理证明自17世纪中叶以来一直是人工智能研究的一个重要领域。莱布尼兹提出了利用机器实现定理证明的想法。19世纪末，G.弗雷格的形式系统为符号逻辑奠定了基础，从而为自动演绎推理提供了理论支持。20世纪50年代，随着数理逻辑的进步和电子计算机的出现，机器定理证明成为了可能。A.纽厄尔和H.A.西蒙通过逻辑理论家系统LT首次实现了命题逻辑中重言式的证明。此后，研究人员开始探索通用的机器定理证明方法，其中归结原理是最具代表性的例子之一。

归结原理是一阶谓词逻辑恒真性问题的一部分解决方案。虽然无法确定是否存在一种算法来判断一阶逻辑中的任何合式公式是否为恒真式，但如果A是恒真式，则必然存在一种算法能够证明这一点。许多一阶逻辑的证明算法都是建立在J.厄尔布朗定理的基础上，其中尤以1965年由J.A.鲁宾逊提出的归结原理最为知名。然而，归结原理并不依赖于特定领域的知识，且不采用针对问题领域的试探法，导致证明过程冗长，难以在合理时间内证明较复杂的数学定理。因此，人们提出了非归结定理证明方法，并重新关注基于试探法的问题求解技术。同时，也有人质疑归结原理的有效性以及所有的自动演绎方法。然而，在信息不全的情况下，或者即使信息齐全，但由于情况众多而无法逐一列举时，只能依靠演绎推理。逻辑程序设计和以PROLOG为原型的日本第五代计算机系统的核心语言，再次确认了归结原理和自动演绎技术的重要性。研究表明，基于认知心理学的试探法和基于逻辑的自动演绎相互补充，缺一不可。自动演绎结合其他技术而不使用归结原理的定理证明技术主要适用于数学定理的机器证明。

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

除了基于经典一阶逻辑的自动演绎技术外，还需要研究高阶逻辑和非标准逻辑中的自动演绎技术，并将其表示形式转换成等价的经典一阶逻辑表示形式，以便实际应用。

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