1 基本概念
1.1 定义
归结法是一种以逻辑公式变形和规则推导为基础的证明方法，常用于判断一个命题或一阶逻辑公式是否可满足，并进一步证明某个结论是否成立。其基本做法是把待证明对象转化为适合机械处理的子句集合，再通过归结规则不断消去互相矛盾的文字，直到推出空子句为止。
1.2 核心思想
归结法的核心在于把复杂证明过程拆解为有限步、可重复执行的推理操作。它不直接从结论正向构造证明，而是借助形式化转换，把问题转为对否定命题的不可满足性检验。
1.2.1 反证法视角
归结法通常采用反证思路：先否定待证结论，再将原前提与否定结论合并处理。如果最终能够导出矛盾，便说明最初的否定不成立，从而原结论成立。这种思路与传统数学中的反证法一致，但在形式上更适合计算机执行。
1.2.2 子句消解机制
在子句层面，归结法依靠互补文字之间的消解来推进证明。例如，一个子句中含有某个命题的正形式，另一个子句中含有其否定形式时，可以将这两部分抵消，生成新的子句。通过反复执行这一过程，推理空间逐渐收缩，最终可能得到空子句。
1.3 适用范围
归结法广泛适用于形式逻辑中的可满足性判断，尤其适合具有明确语法结构、便于标准化处理的逻辑系统。它既可用于命题逻辑，也可用于一阶逻辑。
1.3.1 命题逻辑中的归结
在命题逻辑中，归结法处理的对象是由命题变元及其否定构成的子句。由于没有量词和变量替换问题，推理步骤相对直接，常作为理解归结机制的入门模型。
1.3.2 一阶逻辑中的归结
在一阶逻辑中，归结法需要额外处理变量、谓词、函数符号以及量词变换等问题。此时，推理过程通常要先进行标准化，再通过统一操作使两个子句中的相关文字能够匹配后归结。
2 形式化基础
2.1 逻辑公式与子句
归结法建立在严格的公式表示之上。为了便于自动推理，逻辑公式通常需要转换为规范形式，而子句则是其中最重要的处理单元。
2.1.1 合取范式
合取范式是一种由若干析取式再以合取连接而成的标准表达形式。归结法之所以偏好这种结构，是因为它可以把整体公式拆分成多个相对独立的子句，便于逐一处理。
2.1.2 子句集表示
在实际推理中，公式往往被看作一个子句集。每个子句内部是文字的析取，而整个集合则代表这些子句同时成立。这样一来，推理过程便可视为对集合中元素的系统化操作。
2.2 变量与项
一阶逻辑中的基本构件包括变量、项和各种符号。它们共同决定了公式的结构，也决定了归结时是否能够进行有效匹配。
2.2.1 谓词
谓词用于描述对象之间的性质或关系，是一阶逻辑中的核心语义载体。在归结法中，只有具有相同谓词符号且极性相反的文字，才可能成为归结对象。
2.2.2 函数符号
函数符号用于构造更复杂的项，使逻辑系统能够表达对象之间的生成关系。归结过程中，函数项的存在会增加统一难度，也使推理空间显著扩大。
2.2.3 常量
常量表示固定对象，在公式中通常承担具体实例的角色。它们与变量不同，不会被量化替代，因此在归结和统一中具有更稳定的匹配特征。
2.3 统一与代换
统一是归结法在一阶逻辑中得以成立的关键技术。它用于寻找一个代换，使若干表达式在结构上尽可能一致，从而允许进一步归结。
2.3.1 最一般合一
最一般合一指的是满足统一条件的最弱代换。它不引入多余约束，因此保留了最大的后续推理空间，是一阶归结中最常用、最重要的统一结果。
2.3.2 代换实例化
代换实例化是指用具体项替换变量，使公式成为某种实例。归结法中常通过代换把抽象公式转化为可比较、可消解的形式，从而实现统一后的推导。
3 归结规则
3.1 命题归结
命题归结是归结法最基础的形式，处理对象为命题文字及其否定。它体现了消解互补文字并生成新子句的基本逻辑。
3.1.1 基本归结式
若两个子句分别包含某一命题的正文字与负文字，则可将这对互补文字删除，并把剩余部分合并成新子句。这一规则构成了命题归结的标准形式。
3.1.2 互补文字消去
互补文字消去是归结运算的核心步骤。通过消去相互冲突的部分，推理系统能够不断简化子句集合，并逐步逼近矛盾。
3.2 一阶归结
一阶归结是在命题归结基础上的推广，加入了统一机制，使得带变量的文字也能参与归结。
3.2.1 统一后的归结
在一阶情形下，两个文字能否归结，取决于它们能否通过某个统一代换变得兼容。只有在找到合适的代换后，互补文字才可被消去并生成新的子句。
3.2.2 带量词公式的处理
带量词公式通常不能直接归结，需要先经过量词消去、变量标准化和前束化等处理，再转成子句形式。完成这些预处理后，归结规则才可以直接应用。
3.3 因子化
因子化是归结法中用于简化子句的一类操作，主要针对子句内部出现的可统一重复文字。
3.3.1 重复文字合并
如果一个子句中存在可以统一的相同或相似文字，则可以将它们合并为更简洁的形式。这样做可减少冗余，提高后续归结效率。
3.3.2 归结前简化
因子化常被视为归结前的预处理或辅助步骤。通过提前去除冗余结构，系统可以避免在无效分支上浪费推理资源。
4 证明过程
4.1 标准证明步骤
归结证明通常遵循较为固定的流程，便于算法化实现和结果复现。
4.1.1 公式否定
首先将待证明命题取否定，并与已知前提合并。这样做的目的是把“证明某结论成立”转化为“证明其否定不可满足”。
4.1.2 化为子句集
接下来将所有公式转换为子句集。该过程包括消去蕴含、推进否定、标准化变量以及处理量词等，使公式适合后续归结。
4.1.3 迭代归结
在子句集上反复应用归结规则，每一步都尽量生成新的、更简化的子句。若推导持续进行并最终出现空子句，则证明过程完成。
4.2 空子句与矛盾推出
空子句在归结法中具有特殊地位，通常被看作不可满足性的直接证据。
4.2.1 空子句的意义
空子句不包含任何文字，表示一个不可能成立的析取式。它的出现意味着当前子句集内部存在逻辑矛盾，因此整体公式不可满足。
4.2.2 可满足性判定
如果归结过程能够推出空子句，就说明原公式的否定无法成立，从而原命题可被证明。若推理无法导出空子句，则只能说明当前搜索未完成，未必直接等于可满足。
4.3 证明搜索策略
由于归结可能产生大量中间子句，实际应用中常需要借助搜索策略来控制推理方向。
4.3.1 选择规则
选择规则用于决定优先处理哪些子句或哪些文字。合理的选择能够显著影响搜索效率，有时甚至决定证明是否容易找到。
4.3.2 剪枝与控制
剪枝技术旨在排除明显无效或重复的推理分支，避免搜索空间膨胀。常见做法包括删除冗余子句、限制归结对象以及记录已访问状态。
5 性质与理论结果
5.1 正确性
归结法之所以被广泛采用，一个重要原因在于其形式性质清晰，能够提供可靠的逻辑保证。
5.1.1 可靠性
可靠性指归结规则不会推出错误结论。也就是说，如果某一步推导确实导出了空子句，那么原始公式的不可满足性就可以被信赖。
5.1.2 完备性
完备性表示只要原公式不可满足，归结法在理论上就能够推出空子句。对于自动证明系统而言，这一性质意味着方法不仅安全，而且具有充分的表达能力。
5.2 终止性问题
归结法在理论上完备，但在实际运行中未必总能自动终止，尤其是在一阶逻辑中更为明显。
5.2.1 有限子句集情形
当子句集规模有限且推理空间受控时，归结过程有可能在有限步内完成。此时，若所有可生成子句都已枚举完毕，系统便可判断是否存在矛盾。
5.2.2 非终止与循环
在复杂问题中，归结可能不断生成结构相似的新子句，导致循环或无穷展开。为避免这种情况，通常需要配合策略控制、限制规则或启发式方法。
5.3 复杂度分析
归结法的计算代价较高，尤其在表达能力增强后，搜索开销会迅速上升。
5.3.1 命题逻辑复杂度
命题归结在最坏情况下会出现指数级增长，因为可能需要探索大量子句组合。尽管如此，它仍是许多逻辑求解器的重要基础。
5.3.2 一阶逻辑难度
一阶归结面临更高的理论与实践难度。由于包含统一、实例化和无限展开的可能性，相关问题在计算上往往比命题情形更复杂。
6 应用领域
6.1 自动定理证明
归结法是自动定理证明中的经典工具之一，适合处理形式化程度较高的证明任务。
6.1.1 数学命题验证
在数学命题验证中，归结法可用于检查某些定理、引理或推论是否可由公理系统推出。它尤其适合形式严密、符号清晰的问题。
6.1.2 逻辑系统实现
许多逻辑证明器都以归结为核心机制或重要模块。通过对公式自动转换和搜索，这类系统能够在无需人工逐步干预的情况下完成推理。
6.2 人工智能推理
在人工智能中，归结法常被用作符号推理的基础方法，服务于知识处理与规则推导。
6.2.1 知识表示
归结法要求知识以明确的逻辑形式表达，因此适合结构化知识表示场景。将事实与规则写成子句后，系统便可借助归结进行一致性检查和结论推出。
6.2.2 规则推理
对于由若干条件和结论构成的规则系统，归结法能够通过匹配与消解来逐步触发推断。它在专家系统、推理引擎和符号问答中都有应用价值。
6.3 逻辑程序设计
逻辑程序设计强调以逻辑关系而非命令式流程来描述计算过程，归结法与其有天然联系。
6.3.1 关系表达
在逻辑程序中，很多计算问题会被建模为关系之间的组合与约束。归结法可以把这些关系表达转化为可执行的推理过程。
6.3.2 查询求解
当用户提出查询时，系统可将查询视为待证目标，并通过归结寻找满足条件的实例。若能够归结成功，则查询得到回答或证实。
7 相关变体与扩展
7.1 线性归结
线性归结是一类限制归结路径的策略变体，目的在于减少盲目搜索。
7.1.1 输入归结
输入归结要求归结过程中至少有一个父子句来自初始输入集合。这种限制有助于控制推导层数，使证明更具可追踪性。
7.1.2 目标导向归结
目标导向归结强调从待证目标出发，优先处理与结论相关的子句。它常用于需要明确追踪证明链的场景，逻辑方向更接近“从问题反推答案”。
7.2 支持集策略
支持集策略通过指定一个特殊子集来引导归结过程，从而缩小搜索范围。
7.2.1 选择性推理
系统不必对所有子句一视同仁，而是优先在支持集中进行归结。这样的选择性推理可以减少无关分支，提高效率。
7.2.2 搜索效率优化
支持集方法常与启发式选择结合，借此降低组合爆炸的风险。它在大规模自动证明任务中尤其有实用意义。
7.3 归结的其他扩展
除了基本归结外，研究者还提出了多种扩展形式，以适应更复杂的逻辑系统。
7.3.1 带等式归结
带等式归结处理包含相等关系的公式，通常需要结合重写、替换或专门的等式推理规则。它适用于数学和程序验证中的多种场景。
7.3.2 模态与非经典逻辑中的变体
在模态逻辑、直觉逻辑等非经典系统中，归结法往往需要调整语义和规则形式。虽然具体实现方式不同，但其“转化为可消解结构”的思想仍然具有延续性。
8 历史与发展
8.1 理论起源
归结法的形成与现代数理逻辑、证明论以及计算理论的发展密切相关。
8.1.1 逻辑证明方法的发展
早期逻辑研究主要关注形式系统的严密性和演绎规则的结构化表达。随着逻辑语言不断扩展，研究者逐渐需要一种更适合机械处理的通用证明手段。
8.1.2 自动推理的兴起
计算机出现后，如何让机器自动执行推理成为新的研究方向。归结法因步骤明确、形式统一，迅速成为自动推理领域的重要方法之一。
8.2 重要人物与贡献
归结法的发展离不开多位逻辑学者和计算机科学研究者的推动。
8.2.1 早期形式化研究
早期研究主要集中在如何把证明过程转化为标准化的逻辑操作，并建立可计算的形式框架。这些工作为后来的归结系统奠定了基础。
8.2.2 归结法的成熟与推广
随着统一理论、子句化技术和证明搜索策略的完善，归结法逐渐发展为较完整的自动证明体系，并被广泛传播到人工智能与程序设计相关领域。
8.3 现代影响
归结法至今仍是形式推理的重要工具，其影响延伸到多个计算分支。
8.3.1 计算逻辑中的地位
在计算逻辑研究中，归结法常被视为连接逻辑表达与算法执行的关键桥梁。许多后续方法都在其基础上发展出更高效或更专门化的推理机制。
8.3.2 软件与工具支持
现代逻辑求解器、证明器和符号计算系统中，归结思想仍然随处可见。借助软件工具，归结法不仅用于理论验证，也成为可实际部署的推理技术。