归结原理(卷名：自动控制与系统工程)
resolution principle
将普通形式逻辑中充分条件的假言联锁推理形式符号化，并向一阶谓词逻辑推广的一种推理法则，又称归结法则、分解法则、消解法则。
基本思想 从应用的角度出发，可以从充分条件的假言联锁推理、命题逻辑的归结原理，一阶谓词逻辑的归结原理等三个方面来分析归结原理的基本思想。
充分条件的假言联锁推理 是前提和结论全部由充分条件假言判断构成的一种推理形式。下面是普通形式逻辑中在引入蕴涵连接词“→”（代表如果……则……的逻辑关系）后的推理图式：
横线上、下方的逻辑公式分别与推理的前提和结论相对应。由于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的不可满足性,即应用归结法则和合一算法，反复推求两子句的归结式（对命题逻辑情形无需采用合一算法）,直到最终推导出空子句□,即表明定理得证或问题有解。这个推理过程由计算机自动进行。
应用举例 表说明归结法则在自动演绎中的应用。
根据归结原理进行推理时只需要一条推理规则，即求两子句归结式的归结法则，所以使用简便，容易在计算机上实现。后来发现对于复杂的推理问题，中间归结式的产生会陷入盲目状态，缺乏可以明确遵循的搜索策略,使推理效率大为降低。为此又提出一些改进方案,如语义归结、锁归结、线性归结等，此外还对广义归结进行了研究。
参考书目
中国人民大学哲学系逻辑教研室编:《形式逻辑》,中国人民大学出版社，北京，1984。Ching-Liang Chang and Richard Char-Tung Lee， Symbolic Logic and Mechanical Theorem Proving，Academic Press,Inc.,New York,1973.