[科普中国]-归结原理

归结（resolution）原理，在数理逻辑和自动定理证明中（GOFAI涉及的主题），是对于命题逻辑和一阶逻辑中的句子的推理规则，它导致了一种反证法的定理证明技术。将普通形式逻辑中充分条件的假言联锁推理形式符号化，并向一阶谓词逻辑推广的一种推理法则，又称归结法则、分解法则、消解法则。

命题逻辑在命题逻辑归结原理的推理图式中，P、Q和R称为原子公式（简称原子），即不使用逻辑连接词的简单命题形式。原子和原子的否定式统称句元，例如P与塡P、Q与塡Q、R与塡R即是三对互补句元。子句就是将不同句元用析取词∨（或）连接而成的析取式。应用归结法则进行推理时，所有判断都写成子句的形式，这不论对命题逻辑还是对一阶谓词逻辑都不例外。

在命题逻辑中，原子被看成一个内部结构不予分析的逻辑基元，代表简单的命题形式。单凭普通形式逻辑中充分条件的假言联锁推理的符号化，只能直接演变为命题逻辑的归结原理。命题逻辑的归结原理或归结法则可归纳如下：对任意两个子句H1和H2，如果H1和H2中各自包含一个互补的句元L1和L2（例如上述图式中的Q和塡Q），则可以删去L1和L2，并将原来的子句H1与H2归结为删去互补句元后两子句余下部分的析取式C。C也以子句形式出现，称为原来两子句（常称为亲子句）的一个归结式例如图式中塡P∨R即为塡P∨Q与塡Q∨R两子句的一个归结式。归结原理或归结法则即因此得名。1

一阶谓词逻辑一阶谓词逻辑中，原子是由谓词和项组成的，因而在句元和子句中就有个体变元出现。由于存在量词能用斯科林变换消去，可以认为句元和子句中的个体变元只受全称量词约束 （见逻辑表示）。两个子句H1与H2的归结式可分四种情形：①子句H1与H2的归结式；②子句H 1与子句H2的因子句H2′的二元归结式；③子句H 1的因子句H1′与子句H2的二元归结式；④子句H1、H2各自的因子句H1′与H2′的二元归结式。求子句的因子句和求两子句归结式时，都必须用合一算法求出最普遍合一替换mgu（most general unifier），或称最广通代。这是在一阶谓词逻辑中应用归结法则的关键技术，最普遍合一替换是在一个表达式集合E={E1，…，Ek}中，用一组项（t1，…，tk）替换一组互异个体变元（x1，…，xk），使替换后的各表达式相等（称为合一）的最简替换。①求子句因子句时的最普遍合一替换：例如子句H1=P(x）∨P(f(y））∨塡Q(x) 的因子句H1′=P(f(y））∨塡Q(f(y）），mgu={f(y)/x}。②求两子句（包括子句之一或两子句都有因子句的情形）的二元归结式时的最普遍合一替换：例如子句H 2=塡P(f(g(a））∨R(b），则H2与上例H1的因子句H1′的二元归结式C =塡Q(f(g(a））∨R(b),mgu={g(a)/y}。

应用方法应用归结原理证明定理或求解问题时采用反证法，即先假设与结论相反的命题是成立的，然后根据前提和否定结论的假设（都以子句形式出现），求出一系列中间结论（以归结式的形式出现），如果最后得到两个相互矛盾的命题（以互补句元形式出现的一对单句元子句），即表明与结论相反的假设不能成立，因而原结论的正确性得证，此时归结式是空子句□。可以从理论上证明一阶谓词逻辑的归结原理是完备的，即一个子句集 S（前提和结论否定式合取形成的全体子句）不可满足的充要条件是从子句集S 中能推导出空子句。1

实施步骤应用归结法则的具体步骤是：①将定理或问题用逻辑形式表示。②消去存在量词，使公式中出现的所有个体变元只受全称量词约束。③构造子句集，包括将所有前提表示为子句形式；将结论否定也表示为子句形式。④证明子句集S的不可满足性，即应用归结法则和合一算法，反复推求两子句的归结式（对命题逻辑情形无需采用合一算法），直到最终推导出空子句□，即表明定理得证或问题有解。这个推理过程由计算机自动进行。2

应用举例表说明归结法则在自动演绎中的应用。

根据归结原理进行推理时只需要一条推理规则，即求两子句归结式的归结法则，所以使用简便，容易在计算机上实现。后来发现对于复杂的推理问题，中间归结式的产生会陷入盲目状态，缺乏可以明确遵循的搜索策略，使推理效率大为降低。为此又提出一些改进方案，如语义归结、锁归结、线性归结等，此外还对广义归结进行了研究。1

本词条内容贡献者为:

程鹏 - 副教授 - 西南大学