自动定理证明

人工智能研究领域中的课题

自动定理证明是人工智能研究领域中的一个非常重要的课题，其任务是对数学中提出的定理或猜想寻找一种证明或反证的方法。因此，智能系统不仅需要具有根据假设进行演绎的能力，而且也需要一定的判定技巧。

发展历史

1956年，Newell，Shaw和Simon给出了一个称为“逻辑机器”的程序，证明了罗素、怀德海所著《数学原理》中的许多定理，这标志着自动定理证明的开端。

1959年，Gelernter给出了一个称为“几何机器”的程序,能够做一些中学的几何题，速度与学生相当。

1960年,美籍华裔王浩在IBM704上,编程实现了三个程序，第一个程序用于命题逻辑，第二个程序让机器从基本符号出发自动生成合适命题逻辑公式并选出其中定理，第三个程序用于判定一阶逻辑中的定理。他证明了罗素、怀德海《数学原理》中的几乎所有定理。他的方法人们称之为“王浩”算法。他的这项工作在1984年首届自动定理证明大会上获最高奖—“里程碑”奖。

1960年，Davis、Putnan等给出了D一P过程，大大简化了命题逻辑的处理。

1965年，Robinson提出一归结方法，使得自动定理证明领域发生了质的变化。

1968年，苏联Maslov提出了逆向法，是苏联人六、七十年代在该领域做的主要工作。

归结方法有许多重要改进，每种改进有各自的优点。语义归结由Slagle提出，它将超归结(Robinson)、换名

归结(Meltzer)、支架集策略(Wos，RobinSon)等方法一体化。锁归结，由Boyer在1971年提出，是一个很高效的规则。线性归结由Loveland和Luckham在1970年独立提出。

证明系统

用谓词演算公式描述的事实即证明系统中的公理(axioms)。证明系统(proof system)是应用公理演绎出定理(theorems)的合法演绎规则的集合。所谓演绎，也叫归约(deduction)，是对证明系统中合法推理规则的一次应用。在一个简单的演绎步骤中，可以从公理导出结论(conclusion)，中间可以利用这些规则演绎出的定理。

证明(proof)是个语句序列，以每个语句得到证明而结束，即每个句子要么演绎成公理，要么演绎成前此导出的定理。一个证明若有N个语句(命题)则称N步证明，反驳(refutation)是一个语句的反向证明。它证明一个语句是矛盾的，即不合乎给定的公理。

同一命题的正向证明和反驳有时会有天壤之别，证明长度和复杂性差别很大。构造一个证明或反驳要有深入的洞察、联想，还要有点灵感。

一个语句若能从公理出发推演出来，则称合法语句。任何合法语句也叫做定理(theorem)。从某一公理集合导出的所有定理集合称为理论(theory)。一般说来,理论具有一致性，它不包含相互矛盾的定理。

模型

从公理集合中导出定理集称之为理论。有了理论要解释它的语义必须借助某个模型(model)。因为形式系统只是符号抽象，借助模型可为每个常量、函数、谓词符号找到真理性的解释，即定义每个论域，并表明域上成员和常量公理之间的关系。公理的谓词符号必须派定为域中对象的性质，函数派定为对域中对象的操作。不一致的理论就没有模型，因为无法找到同时满足相互矛盾定理的解释。

公理集合一般情况下只是定义的部分(偏)函数和谓词，是问题域的一个侧面。所以能满足该理论的模型往往不止一个。

证明技术

谓词演算具有完整性，理论上可做出自动生成程序,并证明按公理集合建立的任何理论。它们是公理集合的逻辑结论。但实际做起来，要找到切题的证明如同大海捞针，效率难以容忍。

即使把问题限制在证明单个命题，关键仍然是效率。如果从公理出发做出每一个步骤，在新的步骤上仍然要查找每一个公理找出可能的推理。如此下去就形成一个庞大的树行公理集，每层的节点都是表示一个公理的语句，其深度和宽度随问题和最初给出的公理而定，一层一步骤，N层的树就是N步推理。

归结定理证明

归结法是命题演算中对合适公式的一种证明方法。为了证明合适公式F为真，归结法证明￢F恒假来代替F永真。归结原理是：设有前题L∨P和￢L∨R则其逻辑结论是P∨R，因为两个子句中含有一个命题的正逆命题(L,￢L)。若L为真￢L一定为假，P若为真，P∨R也为真。若L为假，￢L为真，P若为真，P∨R也为真。这个推理把两子句合一(unification)并消去一对正逆命题，故归结，也译做消解。归结证明的过程称为归结演绎。其步骤如下：

[1]把前题中所有命题换成子句形式。

[2]取结论的反，并转换成子句形式加入[1]中的子句集。

[3]在子句集中选择含有互逆命题的命题归结。用合一算法得出新子句(归结式)再加入到子句集。

[4]重复[3]，若归结式为空则表示此次证明的逻辑结论是矛盾，原待证结论若不取反则恒真，命题得证，否则继续重复[3]。

Horn子句实现超级归结

Horn子句是至多只有一个非负谓词符号的子句。这就等于通过谓词演算一个语句只包含一个蕴含运算符连接前题和结论，前题是由‘∧’连接的几个谓词，结论就是单一的谓词符号。

Horn子句形式示例如下:

￢P∨ ￢Q∨S∨ ￢R∨ ￢T （1）

其中只有一个非负谓词S，可作以下演算，先将S移向右方

┠S∨￢P∨￢Q∨ ￢R∨ ￢T （2）

按德·摩根定律

┠ S∨￢ (P∧Q∧R∧T) （3）