命题归结处理固定原子，一阶归结还需要确定怎样替换项才能完成一次推理，以及存在见证依赖于哪些全称变量。FIT3080 第二份逻辑讲义依次介绍替换、合一、子句转换、归结和完整定理证明例子；本篇沿用这条路线，并补足正确性所需的条件 [1][1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5.。

语法和量词规则见形式逻辑与自然演绎，子句与反驳的基础见命题逻辑的自动推理。除特别说明外，这里讨论不含内建等号的经典一阶逻辑，使用非空论域和普通有限项。等号需要额外处理，后文会说明。

替换：一致地替换变量

替换是从变量到项的有限映射。写作 θ={x↦a,y↦f(z)}\theta=\{x\mapsto a,y\mapsto f(z)\}，用 EθE\theta 表示把它应用于表达式 EE。同一变量的各个自由出现必须得到相同替换；在量词内操作时还要避免捕获。

替换同时进行。例如，θ={x↦y,y↦a}\theta=\{x\mapsto y,y\mapsto a\} 时，

R(x,y)θ=R(y,a),R(x,y)\theta=R(y,a),

结果不是 R(a,a)R(a,a)。为 xx 插入的项不会再次被同一替换递归处理。替换复合是另一种操作，约定 E(θσ)=(Eθ)σE(\theta\sigma)=(E\theta)\sigma。若 θ={x↦y}\theta=\{x\mapsto y\}，σ={y↦a}\sigma=\{y\mapsto a\}，则 x(θσ)=ax(\theta\sigma)=a，但 x(σθ)=yx(\sigma\theta)=y，顺序会影响结果。

归结两个子句之前，要把变量分别标准化改名。一个子句中的全称变量 xx，不与另一个子句恰好同名的 xx 共享自由参数身份。先为第二个子句换上新变量名，可以避免无意的绑定关系阻碍本来合法的推理。

合一与最一般合一子

若替换 θ\theta 使两个表达式在语法上完全相同，它就是一个合一子。最一般合一子 MGU 不施加多余限制：就问题中的变量而言，任何其他合一子都可以通过进一步实例化它得到。

例把合一变成项方程

合一 R(x,f(y))R(x,f(y)) 与 R(g(a),f(b))R(g(a),f(b))。谓词及元数一致，剩下 x=g(a)x=g(a) 和 f(y)=f(b)f(y)=f(b)。把后一个方程分解成 y=by=b，得到 MGU：

θ={x↦g(a), y↦b}.\theta=\{x\mapsto g(a),\ y\mapsto b\}.

两个表达式都变为 R(g(a),f(b))R(g(a),f(b))。相反，当 a,ba,b 是不同常量符号时，R(x,x)R(x,x) 与 R(a,b)R(a,b) 无法合一，因为同一变量不能同时替换成两个不同的语法项。这是语法匹配的限制，并没有假设不同名字在每个解释中一定表示不同对象。

一个合一过程维护待解项方程及当前替换，基本操作如下：

  1. 两边已经相同的方程直接删除。
  2. 函数符号和元数一致时，分解成对应参数之间的方程。
  3. 把变量方程定向为 x=tx=t。若 xx 不出现在 tt 中，就把其余方程及已经记录的替换项中的 xx 都换成 tt。
  4. 函数符号或元数不匹配，或者出现检查失败时，报告无法合一。

出现检查会拒绝 x=f(x)x=f(x)：普通有限项不可能等于一个真包含自身的复合项。某些程序系统允许循环项，那使用的是不同的项语义，不属于这里定义的合一问题。对有限一阶项，标准合一算法会终止，并返回 MGU 或失败。

例一个绑定会进一步确定另一个绑定

方程 x=f(y)x=f(y)、y=ay=a 先为 xx 提供一个暂定绑定，解出 yy 后还需更新它。最终替换为 {x↦f(a),y↦a}\{x\mapsto f(a),y\mapsto a\}。如果只把两次绑定并排记下来，却不把后者传播进前者，就没有得到这个规范化的同时替换。

从量化公式到子句

要证明 K⊨qK\models q，就反驳 K∧¬qK\land\neg q。对有限一阶知识库和句子查询，可以采用以下预处理流程：

  1. 消去 →\to 与 ↔\leftrightarrow。
  2. 把否定推进到原子，必要时使用量词否定律。
  3. 改名约束变量，避免不同量词重复使用同一名字。
  4. 在满足自由变量限制的前提下，把量词移到前束位置。
  5. 引入新的 Skolem 符号消去存在量词，保留正确的全称变量依赖。
  6. 把剩余矩阵变成 CNF。
  7. 将剩余变量视为全称量化，拆开合取，并让不同子句的变量分别改名。

Skolem 化保持的是扩展符号表下的可满足性，不是原符号表中的逐式逻辑等价。“删去全称量词”只是子句记法约定，不是把全称变量变成常量或存在变量。直接分配得到 CNF 仍可能很昂贵，因此这是便于学习的流程，不是优化实现的完整方案。

Skolem 函数记录见证的依赖

比较

∀x∃y R(x,y)与∃y∀x R(x,y).\forall x\exists y\,R(x,y) \qquad\text{与}\qquad \exists y\forall x\,R(x,y).

第一式引入新函数 ff，得到 ∀x R(x,f(x))\forall x\,R(x,f(x))，因为见证可以依赖 xx。第二式引入新常量 cc，得到 ∀x R(x,c)\forall x\,R(x,c)，因为同一个见证必须适用于所有 xx。若把第一式中的 f(x)f(x) 换成常量，就额外施加了原命题没有要求的限制。

为什么可满足性得到保留？Skolem 化后公式的模型通过新函数或常量提供见证，忘掉这些新符号，仍是原句子的模型。反过来，在通常的模型论背景假设下，可以为原句子的模型选择适当见证，把它扩展为新符号表的模型。不能随意复用已有符号，否则可能在见证之间强加原先没有的关系。

例拆分子句后仍要保留依赖

考虑

∀x∃y (R(x,y)∧¬S(x,y)).\forall x\exists y\, \bigl(R(x,y)\land\neg S(x,y)\bigr).

Skolem 化后的子句可写为

{R(x1,f(x1)),¬S(x2,f(x2))}.\{R(x_1,f(x_1)),\quad\neg S(x_2,f(x_2))\}.

两个子句的变量已经分别改名，但 Skolem 函数仍是同一个 ff。若各子句又分别更换函数名，就丢掉了“对每个输入，同一个见证须同时满足两个条件”的要求。

一阶归结

设 C∨LC\lor L 与 D∨¬MD\lor\neg M 的变量已经分别改名，原子 L,ML,M 的 MGU 为 θ\theta。二元归结得到

C∨LD∨¬M(C∨D)θ.\frac{C\lor L\qquad D\lor\neg M} {(C\lor D)\theta}.

替换必须应用于整个剩余归结式，不能只处理被消去的文字。可靠性的理由是：全称量化的父子句允许取相应替换实例，而命题归结对这些实例保持真值。

例带变量的规则怎样用于具体事实

把 ¬P(x)∨Q(x)\neg P(x)\lor Q(x) 与 P(f(a))P(f(a)) 归结。选中原子的合一子是 {x↦f(a)}\{x\mapsto f(a)\}，结果为 Q(f(a))Q(f(a))。若保留一个未实例化的全称变量，直接写成 Q(x)Q(x)，就把结论无根据地加强了。

标准完备一阶归结系统除了二元归结，还使用因子化。若一个子句内的同号文字可以合一，就把 MGU 应用于整个子句，再合并这些文字。例如，P(x)∨P(y)P(x)\lor P(y) 在 {y↦x}\{y\mapsto x\} 下可因子化为 P(x)P(x)。这不只是删去原本完全相同的重复项，而是通过合一得到一个有用实例。通常的反驳完备性结论依赖完整规则系统和适当的公平搜索，不能直接归给任意二元归结序列。

因子化保持可靠性，因为全称量化的子句蕴含每个替换实例；应用合一替换后，相同文字的重复析取与保留一份具有相同真值。一般的一阶归结反驳完备性仍依赖 Herbrand 定理与提升引理，本文尚未证明这两项结果。下面的具体反驳证明不能代替该元定理的证明。

完整证明一个存在查询

例从供应规则推出认证对象存在

使用常量 aa、一元谓词 A,CA,C 和二元谓词 RR，前提为

A(a),A(a),∀x(A(x)→∃y (R(x,y)∧C(y))).\forall x\bigl(A(x)\to \exists y\,(R(x,y)\land C(y))\bigr).

可以把 A(x)A(x) 理解为“xx 是获批供应者”，R(x,y)R(x,y) 为“xx 提供 yy”，C(y)C(y) 为“yy 通过认证”。目标是 ∃z C(z)\exists z\,C(z)。

对规则先消去蕴涵，再把存在量词移到析取外，因为 yy 不自由出现在 A(x)A(x) 中。引入新的 Skolem 函数 f(x)f(x)，把 CNF 拆成两个子句，并保留同一个 ff。否定目标后得到 ∀z ¬C(z)\forall z\,\neg C(z)。

子句公式来源
1A(a)A(a)事实
2¬A(x1)∨R(x1,f(x1))\neg A(x_1)\lor R(x_1,f(x_1))Skolem 化的规则
3¬A(x2)∨C(f(x2))\neg A(x_2)\lor C(f(x_2))Skolem 化的规则
4¬C(z)\neg C(z)目标的否定
5C(f(a))C(f(a))归结 1、3，x2↦ax_2\mapsto a
6□\square归结 4、5，z↦f(a)z\mapsto f(a)

空子句反驳了目标的否定，因而证明认证对象存在。扩展语言中用 f(a)f(a) 指向一个见证，但原理论没有预先命名这个对象。第 2 个子句是合法输入，却不是回答当前查询所必需的；搜索过程不要求使用每个前提。

搜索策略与终止性的边界

有限命题变量只能组成有限多个不同子句。一阶函数符号却可以产生没有上界的项，例如 a,f(a),f(f(a)),…a,f(a),f(f(a)),\ldots，所以不断生成新子句的搜索可能始终无法饱和。

经典一阶逻辑的有效性是半可判定的：完备且公平组织的证明搜索，在句子有效时最终能找到证明，但在无效时未必终止。对应地，在满足完备性条件时，归结最终能反驳不可满足的子句集；对子句集可满足的输入，则可能无限运行。可靠性与完备性不意味着存在适用于所有一阶输入的判定过程 [2][2] OpenLogicProject, The Open Logic Text. 2026. Complete build, revision 9620cc7, July 12, 2026; CC BY 4.0. https://builds.openlogicproject.org/open-logic-complete.pdf。

FIT3080 还介绍了几种引导归结搜索的方法。它们各自的限制需要明确：

方法作用与条件
单位优先优先尝试短子句或单位父子句，但不能让必要推理永远得不到执行
单位归结每一步都要求单位父子句；对任意子句集并不完备
支持集策略至少一个父子句来自支持集或其后代；通常的完备性保证要求支持集之外的子句可满足
输入归结每一步都使用一个原始输入子句作为父子句；对一般子句集不完备
包摄删除删去已被更一般的保留子句涵盖的冗余子句；判断包摄本身也有成本

例如，P(x)P(x) 包摄 P(a)∨Q(a)P(a)\lor Q(a)，因为前者的一个实例是后者的子集。删除冗余子句时仍应保留证明来源。把否定目标设为初始支持集，在其余知识库可满足时很有用；若知识库本身已矛盾，就不能自动沿用这一完备性理由。

等号、逻辑编程与 SMT

逻辑包含内建等号时，仅把等号当作普通谓词来归结，不能捕捉其全部性质。需要加入等号公理，或使用参数归结、超位置等专门规则。例如，在对象同一性的语义下，a=ba=b 和 P(a)P(a) 后承 P(b)P(b)；若把等号当作无关关系，就会漏掉这种连接。

一阶确定子句还通向逻辑编程与 SLD 归结。一个过程可能保持可靠，却因为反复选择同一递归分支而循环。普通深度优先 Prolog 搜索没有无条件的终止或完备保证。无函数符号、有限论域等限制可以带来更强的终止性质，但必须明确指出这些条件。

SMT 在命题搜索之外，加入指定理论的推理，例如线性算术、带未解释函数的等式或数组。它不是解决任意一阶逻辑的万能方法。保证取决于所支持的理论片段，带量词或困难输入可能得到 unknown。这些是课程入门路线之后的延伸，不是理解前述例子的先决条件 [3][3] C. Trippel and H. Lachnitt, “CS 257: Introduction to Automated Reasoning,” 2026. Winter 2026 course: propositional reasoning, first-order resolution and unification, and satisfiability modulo theories. https://web.stanford.edu/class/cs257/。

证明证书需要留下什么

每个派生子句应记录父子句编号、改名后的变量、被归结或因子化的文字，以及替换。检查器验证替换确实让选中表达式合一，并检查归结结果是否正确。预处理也需要检查，包括 Skolem 符号是否新鲜、参数依赖是否正确；对错误编码作出的正确反驳，仍不能证明原问题。

找到反驳时，返回已经检查的证明；若报告模型，则对照原始句子验证。时间或资源耗尽应返回“未知”，而不是“假”。这是把一次证明搜索演示变成可核对定理证明流程所需的基本区分。

练习

练习求一个 MGU

合一 R(x,f(x))R(x,f(x)) 与 R(g(y),f(g(a)))R(g(y),f(g(a)))。写出 MGU，并检查两个表达式替换后的结果。

查看解析
解

参数方程给出 x=g(y)x=g(y) 和 x=g(a)x=g(a)，因此 y=ay=a。一个 MGU 是 {y↦a,x↦g(a)}\{y\mapsto a,x\mapsto g(a)\}，两边都成为 R(g(a),f(g(a)))R(g(a),f(g(a)))。

练习保留见证依赖

对 ∀x∃y∀z∃w T(x,y,z,w)\forall x\exists y\forall z\exists w\,T(x,y,z,w) 做 Skolem 化。在标准构造中，新函数需要哪些参数？

查看解析
解

使用新函数 f,gf,g，得到 ∀x∀z T(x,f(x),z,g(x,z))\forall x\forall z\,T(x,f(x),z,g(x,z))。yy 的见证依赖前面的全称变量 xx，ww 的见证可以依赖前面的全称变量 x,zx,z。之前的 yy 已由 f(x)f(x) 表示，不必再单独添加一个存在变量参数。

练习发现遗漏的替换

有人把 ¬R(x,y)∨S(y)\neg R(x,y)\lor S(y) 与 R(a,f(a))R(a,f(a)) 归结，写出 S(y)S(y)。修正这一步。

查看解析
解

MGU 是 {x↦a,y↦f(a)}\{x\mapsto a,y\mapsto f(a)\}，还要应用于剩余文字，因此结果为 S(f(a))S(f(a))。若留下全称变量 yy，就会声称所有对象都满足该谓词。

练习解释尚未结束的运行

一个不受片段限制的一阶证明器不断生成新项，却没有找到矛盾。完备性是否意味着它最终一定会报告一个满足模型？

查看解析
解

不是。反驳完备性保证对不可满足输入，在公平搜索下最终能找到反驳；它不保证可满足输入的终止或模型输出。没有独立检查的模型，或适用于该片段的完备判定过程，就只能保留“未知”状态。

反例单位归结与输入归结为何不完备

四个子句 P∨QP\lor Q、P∨¬QP\lor\neg Q、¬P∨Q\neg P\lor Q、¬P∨¬Q\neg P\lor\neg Q 联合不可满足，因为每个赋值都会使其中一个子句为假。没有单位子句，单位归结连第一步都无法进行。输入归结可以导出单位子句，但要在最后一步得到空子句，两个父子句必须是互补的单位子句；二者都不是原始输入，因而这一步被禁止。不加这两种限制时，前两个子句归结得到 PP，后两个得到 ¬P\neg P，再归结即可得到空子句。

参考文献

  1. [1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5. ↩
  2. [2] OpenLogicProject, The Open Logic Text. 2026. Complete build, revision 9620cc7, July 12, 2026; CC BY 4.0. https://builds.openlogicproject.org/open-logic-complete.pdf ↩
  3. [3] C. Trippel and H. Lachnitt, “CS 257: Introduction to Automated Reasoning,” 2026. Winter 2026 course: propositional reasoning, first-order resolution and unification, and satisfiability modulo theories. https://web.stanford.edu/class/cs257/ ↩