将普通形式逻辑中充分条件的假言联锁推理形式符号化，并向一阶谓词逻辑推广的一种推理法则，又称归结法则、分解法则、消解法则。

简介

基本思想

命题逻辑的归结原理

一阶谓词逻辑的归结原理

应用方法

实施步骤

应用举例

简介

归结原理是一种推理规则。从谓词公式转化为子句集的过程中看出，在子句集中子句之间是合取关系，其中只要有一个子句不可满足，则子句集就不可满足。若一个子句集中包含空子句，则这个子句集一定是不可满足的。归结原理就是基于这一认识提出来的。

他的原理就是：

P->Q, Q->R 则 P->R

由于 P->Q 就是 ￢P∨Q

而 Q->R 就是 ￢Q∨R

所以，他相当于将Q 和 ￢Q合并。也就是说，

P∨{∑1} 与 ~P∨{∑2}

可以归结为 {∑1}∨{∑2}

其中∑1,∑2是文字的集合

基本思想

从应用的角度出发，可以从充分条件的假言联锁推理、命题逻辑的归结原理，一阶谓词逻辑的归结原理等三个方面来分析归结原理的基本思想。

充分条件的假言联锁推理 是前提和结论全部由充分条件假言判断构成的一种推理形式。下面是普通形式逻辑中在引入蕴涵连接词“→”（代表如果……则……的逻辑关系）后的推理图式：横线上、下方的逻辑公式分别与推理的前提和结论相对应。

由于P→Q (如果P 则Q)（非P或Q）这两个公式逻辑等价，即（P→Q）呏（塡P∨Q）,同理有（Q→R）呏（塡Q∨R）,（P→R）呏（塡P∨R）。用这些逻辑等价关系的右式分别替换其中的蕴涵公式，即得命题逻辑中使用归结法则的推理图式：

命题逻辑的归结原理

在命题逻辑归结原理的推理图式中，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两子句的一个归结式。归结原理或归结法则即因此得名。

一阶谓词逻辑的归结原理

一阶谓词逻辑中，原子是由谓词和项组成的，因而在句元和子句中就有个体变元出现。由于存在量词能用斯科林变换消去，可以认为句元和子句中的个体变元只受全称量词约束 (见逻辑表示)。两个子句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 中能推导出空子句□。

实施步骤

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

应用举例

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

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