归结原理（Resolution）

归结原理（Resolution Principle）是一种用于自动定理证明的推理规则，它只依靠单一的归结推理即可对命题逻辑和一阶逻辑进行完备的反驳式证明。该原理由美国逻辑学家约翰·艾伦·罗宾逊（John Alan Robinson）于1965年提出。

概述

归结采用反证法思路：要证明某公式为定理，先假设其否定，将全部前提与被否定的结论化为合取范式，拆成若干子句。随后不断挑选含互补文字的两个子句做归结，生成新的归结式并加入子句集。若最终推导出空子句（矛盾），则说明原假设不可满足，从而原命题成立。

核心原理

归结的关键在于合一（unification）与文字消解。

• 子句范式：任何一阶公式都可经前束化、斯科伦化转为子句集，保持可满足性等价。
• 互补文字：两个子句中若分别含有某文字及其否定，即可归结掉这对文字。
• 合一算法：在一阶情形下，需为变量寻找最一般合一子，使互补文字的谓词项完全匹配。
• 空子句：归结出不含任何文字的空子句，代表逻辑上的假，宣告反驳成功。

归结方法是反驳完备的：若子句集不可满足，则一定存在一条归结推导得到空子句。为提高效率，人们又提出了线性归结、单元归结、输入归结、SLD归结等受限策略。

应用场景

归结原理是逻辑程序设计语言Prolog的执行内核，其SLD归结配合霍恩子句实现了高效的目标求解。它还广泛用于自动定理证明系统、专家系统的推理引擎、知识库一致性检查，以及形式化验证中的可满足性判定。

常见问题

问：归结为什么要先取结论的否定？答：因为归结本质是反驳法，只能证明子句集不可满足。把结论取否定后并入前提，若能导出矛盾（空子句），就反证了原结论必然成立。

问：归结在一阶逻辑中一定会停机吗？答：不一定。一阶逻辑只是半可判定的，若公式确为定理，归结终会找到空子句；但若不是定理，过程可能永不终止。