什么是定理机器证明?

[拼音]：dingli jiqi zheng ming

[外文]：mechanical theorem proving

用计算机自动地进行推理和证明定理。所谓定理，并不限于数学的，凡是用演绎法推导的论断都可以看作是定理。定理证明是人工智能研究中的一个基本课题，广泛应用于各种人工智能系统，例如问题求解系统、答问系统、自动程序设计、自动情报检索和各种数学系统。

（1）归结方法：归结是定理机器证明的一个重要方法，1965年由J.A.鲁宾逊建立。例如以P、Q、R、S分别代表四种陈述，-P表示P不真，P∨Q表示P和Q至少有一个为真。最简单的归结原理就是:由P∨Q和-P∨R可推出Q∨R。假定已知事实：-P∨-Q、Q∨R∨-S、P、S，欲证R成立。归结方法总是使用反证法，因此，假定要证的定理不成立，即假定-R。把P-∨-Q和Q∨R∨-S相归结得-P∨R∨-S，以此与-R归结得-P∨-S，再与P归结得-S，结果与S矛盾，故定理得证。

（2）自然推导：归结方法及其改进过于一般化，故效率不高。人在某一领域内证明定理是用自然推导法，即除一般的逻辑推导外还利用他在这一领域中的知识和经验。模仿人的这种自然推导法的最初成果是1963年A.纽厄尔、J.C.肖和H.A.西蒙的LT系统。另外，还有以归结方法与自然推导相结合的系统。

（3）判定方法：在较小的领域内找一个有效的判定方法来作定理证明也受到人们的重视。这方面最早的工作是A.塔斯基的初等代数和初等几何的判定方法。这种方法虽效率很低，但后来又有人作了不少改进。王浩给出命题逻辑的一个很有效的判定方法。吴文俊提出的关于初等几何和微分几何的判定方法也是很成功的。

参考书目

C. Chang and R. C. Lee， Symbolic Logic and Mechanical Theorem Proving， Academic Press，New York，1973.