📑 本页目录（点开跳转）
05 · 推理与分辨率
⏱ 34 分钟 ｜ ⭐⭐ 一条规则打天下：把所有公式压成子句，然后推出空子句
🎯 一句话
想证明 φ，就把 φ 的否定塞进知识库，然后用一条规则反复消字母——推出「空子句」，就等于把所有可能世界都堵死了，于是 φ 必然成立。
第 4 章告诉你假言推理不够用，而真值表要查 2ⁿ 个世界。这一章给出实际能用的那条路。
🧰 一、先备好等价律
推理之前要先整形：把公式变成一种标准写法。整形靠的是等价律——第 4 章说过，等价就是模型集相同，所以换写法不改变任何东西。
| 名字 | 等价式 |
|---|---|
| 消去蕴含 ⭐ | φ → ψ ≡ ¬φ ∨ ψ |
| 消去双蕴含 | φ ↔ ψ ≡ (φ → ψ) ∧ (ψ → φ) |
| 双重否定 | ¬¬φ ≡ φ |
| 德摩根律 ⭐ | ¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ ¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ |
| 分配律 ⭐ | (φ ∧ ψ) ∨ χ ≡ (φ ∨ χ) ∧ (ψ ∨ χ) |
| 逆否 | φ → ψ ≡ ¬ψ → ¬φ |
⭐ 前三条 + 德摩根负责「把否定往里赶」，分配律负责「把 ∨ 往里赶」。整套 CNF 转换就是这两件事。
🔻 二、否定范式（NNF）：把 ¬ 赶到字母跟前
NNF：否定符号只出现在命题字母的正前面。 文字（literal） = 一个命题字母，或它的否定。例：
P、¬Q是文字，¬(P ∧ Q)不是。
做法：先消去 → 和 ↔，然后反复用德摩根律和双重否定，直到 ¬ 无处可退。
🖐️ 手算
$$\neg(P \vee (\neg R \wedge P))$$
| 步 | 结果 | 用了什么 |
|---|---|---|
| 0 | ¬(P ∨ (¬R ∧ P)) | 原式 |
| 1 | ¬P ∧ ¬(¬R ∧ P) | 德摩根（外层 ∨） |
| 2 | ¬P ∧ (¬¬R ∨ ¬P) | 德摩根（内层 ∧） |
| 3 | ¬P ∧ (R ∨ ¬P) | 双重否定 ✅ NNF |
📐 三、合取范式（CNF）：一切的标准形
子句（clause） = 若干文字的析取，例
¬G ∨ ¬J。 CNF = 若干子句的合取，例(P ∨ Q ∨ ¬R) ∧ (¬S ∨ ¬R)。
⭐ 一个 CNF 就是一张「约束清单」：每个子句是一条约束，说「这几个文字里至少得有一个为真」。满足公式 = 同时满足每条约束。所以 CNF 后面通常直接写成子句的集合，∧ 都省掉。
五步流程：
- 消去 ↔
- 消去 →（
φ → ψ换成¬φ ∨ ψ） - 把 ¬ 推到底（NNF）
- 用分配律把 ∨ 推到 ∧ 的里面
- 展平、清理
🖐️ 手算例 1：一个小的
$$\neg(P \to (Q \vee R))$$
| 步 | 结果 |
|---|---|
| 消去 → | ¬(¬P ∨ Q ∨ R) |
| 德摩根 | P ∧ ¬Q ∧ ¬R |
| CNF | (P) ∧ (¬Q) ∧ (¬R) ✅ 三个单文字子句 |
🖐️ 手算例 2：会用到「丢掉恒真子句」
$$P \vee (\neg Q \wedge (R \to \neg P))$$
| 步 | 结果 |
|---|---|
| 消去 → | P ∨ (¬Q ∧ (¬R ∨ ¬P)) |
| 分配律 | (P ∨ ¬Q) ∧ (P ∨ ¬R ∨ ¬P) |
| ⭐ 清理 | 第二个子句同时含 P 和 ¬P，恒真，删掉 |
| CNF | P ∨ ¬Q ✅ |
⭐ 同时含
L和¬L的子句永远为真，对约束清单毫无贡献，可以直接扔。 这是最常用的化简技巧，考试里几乎每题都会用到一次。
⚠️ 分配律会让公式膨胀
$$(G \vee H) \to (\neg J \wedge \neg K)$$
消去 → 加德摩根后是 (¬G ∧ ¬H) ∨ (¬J ∧ ¬K)，两个二元合取做分配 → 2 × 2 = 4 个子句：
$$(\neg G \vee \neg J) \wedge (\neg G \vee \neg K) \wedge (\neg H \vee \neg J) \wedge (\neg H \vee \neg K)$$
⚠️ m 个合取 ∨ n 个合取 → m×n 个子句，嵌套几层就是指数爆炸。 💡 工程注（讲义之外）：真实 SAT 工具改用引入新变量的转换，得到的公式只保证「同时可满足」而非等价——判定可满足性够用了。
✂️ 四、分辨率规则
$$\frac{\alpha \vee \beta \qquad \neg\beta \vee \gamma}{\alpha \vee \gamma}$$
其中 β 是一个文字。两个子句里有一对互补的文字，就把它们一起消掉，剩下的合并成一个新子句。
⭐ 直觉（一行）：β 要么真要么假。
- β 假 → 第一个子句要靠 α 撑着 → α 真
- β 真 → 第二个子句要靠 γ 撑着 → γ 真
两种情况下 α ∨ γ 都成立，所以它必然为真。这就是这条规则可靠的全部理由。
三个特例，帮你认出它的真面目
| 场景 | 形式 | 说明 |
|---|---|---|
| 推出空子句 ⭐ | β 和 ¬β 分辨 → □ |
两边都没剩下东西，得到矛盾 |
| 就是传递性 | ¬α ∨ β 和 ¬β ∨ γ → ¬α ∨ γ |
换成箭头写：α → β，β → γ ⟹ α → γ |
| 假言推理是它的特例 | P 和 ¬P ∨ Q → Q |
即 P 和 P → Q 推出 Q |
⭐ 空子句 □ 的意思：一个「一个文字都没有」的子句。 子句的意思是「至少有一个文字为真」，空子句要求「在零个文字里至少有一个为真」——这不可能。 所以 □ 代表「假」，推出它就等于推出了矛盾。
🔄 五、⭐ 反证法：整套方法的核心套路
分辨率单独用起来别扭（它只会消文字，不会造新东西）。真正的用法是反证：
要证 KB ⊢ φ，四步： ① 否定结论，把 ¬φ 加进去 ② 全部转成 CNF，得到一堆子句 ③ 反复用分辨率 ④ 推出空子句 □ → 证毕
为什么这样是对的
这一步直接吃第 4 章第五节的结论：
$$KB \models \varphi \iff Mod(KB) \subseteq Mod(\varphi) \iff Mod(KB) \cap \overline{Mod(\varphi)} = \varnothing \iff KB \cup \{\neg\varphi\} \text{ 不可满足}$$
⭐ 翻译成人话：「KB 蕴含 φ」和「KB 加上 φ 的否定之后，一个可能世界都不剩」是同一件事。 文氏图上看更直白：小圈完全套在大圈里 ⟺ 小圈和大圈外面的部分没有交集。
⭐ 这就是为什么逻辑证明总要先「假设结论不成立」。 不是修辞技巧——是因为计算机不擅长「检查所有情况都对」，但很擅长「把所有情况一条条堵死」。
🖐️ 六、完整手算一遍
证明：P → Q，Q → ¬R，P ∨ ¬R ⊢ ¬R
第一步，全部转 CNF（结论要先取否定）：
| 来源 | 原式 | CNF |
|---|---|---|
| 前提 1 | P → Q | ¬P ∨ Q |
| 前提 2 | Q → ¬R | ¬Q ∨ ¬R |
| 前提 3 | P ∨ ¬R | P ∨ ¬R |
| 否定结论 | ¬(¬R) | R |
第二步，反复分辨：
| # | 子句 | 来源 | 消掉了谁 |
|---|---|---|---|
| 1 | ¬P ∨ Q | 前提 | |
| 2 | ¬Q ∨ ¬R | 前提 | |
| 3 | P ∨ ¬R | 前提 | |
| 4 | R | 否定结论 | |
| 5 | P | 3, 4 分辨 | ¬R 与 R |
| 6 | Q | 1, 5 分辨 | ¬P 与 P |
| 7 | ¬R | 2, 6 分辨 | ¬Q 与 Q |
| 8 | □ | 4, 7 分辨 | R 与 ¬R ✅ |
⭐ 推出空子句，证毕。 注意第 7 步得到的 ¬R 正是我们要的结论——但证明还没完：反证法的终点必须是 □，因为我们要的不是「推出了 ¬R」，而是「假设 R 会导致矛盾」。
💡 手算的两个实用习惯： ① 给每个子句编号，每步写清「用了哪两条、消掉了哪个文字」——不然三步之后自己都乱。 ② 优先挑单文字子句（上面的第 4 条
R）去分辨，它一次就能砍掉别的子句里的一个文字，收敛最快。这个策略有名字，叫单元优先。
🎯 七、可靠、反驳完备，但不是「完备」
⚠️ 这里有个容易背错的点，值得单独讲。
| 性质 | 分辨率有没有 | 含义 |
|---|---|---|
| 可靠（sound） | ✅ 有 | 推出来的子句都是真的（第四节那个直觉就是证明） |
| 完备（complete） | ❌ 没有 | 它推不出所有被蕴含的公式 |
| 反驳完备（refutation complete） | ✅ 有 | 子句集不可满足 ⟹ 一定能推出 □ |
⭐ 为什么不完备：P ⊨ P ∨ Q 是成立的，但分辨率只会消文字、不会加文字，从子句 P 永远得不到 P ∨ Q。
⭐⭐ 所以反证法不是「一种可选风格」，而是必需品：分辨率的强项恰好是「证明一堆子句自相矛盾」，那就把所有问题都翻译成这个形状。
$$\text{证 } \varphi \;\longrightarrow\; \text{证 } KB \cup \{\neg\varphi\} \text{ 不可满足} \;\longrightarrow\; \text{推出 } \square$$
代价
⚠️ 分辨率是指数时间的——每一轮都会造出新子句，子句越来越多、越来越长。 命题逻辑可判定（第 4 章），所以这个过程一定会停，但可能停得非常晚。
四条剪枝启发式
| 策略 | 做什么 | 为什么有效 |
|---|---|---|
| 单元优先 ⭐ | 先用只有一个文字的子句 | 一次消掉别人一个文字，收敛最快 |
| 删恒真子句 | 同时含 L 和 ¬L 的直接扔 |
它永远为真，不构成约束 |
| 删被包含子句 | 若存在子句是它的子集，扔掉大的 | 小的约束更强，大的多余 |
| 删纯文字子句 | 某文字 L 出现过、¬L 从没出现 |
它永远消不掉，参与不了任何矛盾 |
🧭 八、这套东西今天在哪儿
⭐ CNF + 子句集 + 反证 就是现代 SAT 求解器的输入格式和工作方式。芯片验证、排班调度、依赖求解（apt / pip 挑版本）、程序验证，底层大多是把问题编成 CNF 丢给 SAT 求解器。
⚠️ 顺手澄清一个高频混淆：LLM 说的「推理」和这一章的「推理」不是一回事。
| 本章的推理 | LLM 的「推理」（思维链） | |
|---|---|---|
| 是什么 | 保真的符号变形 | 生成一段看起来像推理的文本 |
| 保证 | ⭐ 可靠：推出来的必然为真 | ❌ 无任何保证，中间步骤可以是错的 |
| 失败方式 | 推不出来（超时） | 推出错的东西，而且理由写得很像样 |
⭐ 这也是为什么「LLM + 形式化求解器」是一个常见组合：让模型负责把自然语言翻译成约束，让求解器负责保证结论没错。
🔗 这一章连到哪里
| 去哪 | 为什么 |
|---|---|
| 04 · 模型集 | ⭐ 第五节那条「KB ⊨ φ ⟺ KB ∪ {¬φ} 不可满足」全靠那一章的集合定义；不确定为什么反证法合法就回去看那张文氏图 |
| 06 · 一阶逻辑 | 同一套流程加两个零件（Skolem 化和合一）就能处理带量词的公式 |
| 大模型全景导论 09 · 推理范式 | ⭐ 去看第八节那个对比的另一半：思维链、自洽性、ReAct 到底在做什么——它们提升的是「答对的概率」，而不是「保真」 |
| 密码学与信息安全 21 · 零知识证明 | ⭐ 同一个动作的另一处应用：那一章把「程序」编译成算术电路 + R1CS 约束组，和本章把「命题」压成CNF 子句集是一个思路——把语义问题降成约束满足问题。那里的「约束写少了 = 能造假证明」，正是约束清单不完整的后果 |
✅ 检查点
- 什么是文字、子句、CNF？为什么说「一个 CNF 就是一张约束清单」？
- 把
¬(P ∨ (¬R ∧ P))化成 NNF，并把P ∨ (¬Q ∧ (R → ¬P))化成 CNF。后者最后为什么能丢掉一个子句？ (G ∨ H) → (¬J ∧ ¬K)转 CNF 会得到几个子句？这说明分配律有什么问题？- 写出分辨率规则，并用一句话解释它为什么可靠。空子句 □ 为什么代表「假」？
- 反证法四步是什么？它凭什么是对的（写出那条等价链）？
- 手算：
P → Q，Q → ¬R，P ∨ ¬R⊢¬R。推到第 7 步已经得到 ¬R 了，为什么还要走第 8 步？ - 手算：KB = {A → (B ∨ C), A, ¬B}，证明 KB ⊨ C。
- 分辨率是可靠的、反驳完备的，但不是完备的——举出那个反例。为什么这件事使得反证法成为必需品？
- LLM 的「推理」和本章的「推理」差在哪？
👀 答案
- 文字 = 一个命题字母或它的否定；子句 = 若干文字的析取；CNF = 若干子句的合取。说它是约束清单，是因为每个子句要求「这几个文字里至少有一个为真」，满足整个公式 = 同时满足每一条约束——所以 CNF 常直接写成子句的集合，∧ 全省掉。
- NNF：¬(P ∨ (¬R ∧ P)) →（德摩根，外层）¬P ∧ ¬(¬R ∧ P) →（德摩根，内层）¬P ∧ (¬¬R ∨ ¬P) →（双重否定）¬P ∧ (R ∨ ¬P)。CNF：消去 → 得
P ∨ (¬Q ∧ (¬R ∨ ¬P))，分配律得(P ∨ ¬Q) ∧ (P ∨ ¬R ∨ ¬P)；⭐ 第二个子句同时含P和¬P，恒真，删掉，答案 P ∨ ¬Q。 - 4 个：
(¬G∨¬J) ∧ (¬G∨¬K) ∧ (¬H∨¬J) ∧ (¬H∨¬K)。⚠️ 说明 m 个合取 ∨ n 个合取 → m×n 个子句，朴素分配律会指数爆炸（所以真实 SAT 工具改用引入新变量的转换，只保证同时可满足而非等价）。 - 规则：从
α ∨ β和¬β ∨ γ推出α ∨ γ（β 是文字）。可靠是因为 β 要么假（那第一个子句得靠 α）要么真（那第二个得靠 γ），两种情况下α ∨ γ都为真。□ 代表假，因为子句的意思是「至少一个文字为真」，而空子句要在零个文字里找一个为真——不可能。 - ① 否定结论 ② 全部转 CNF ③ 反复分辨 ④ 推出 □。凭据：KB ⊨ φ ⟺ Mod(KB) ⊆ Mod(φ) ⟺ Mod(KB) ∩ Mod(φ) 的补集 = ∅ ⟺ KB ∪ {¬φ} 不可满足。⭐ 图上就是「小圈套在大圈里 ⟺ 小圈和大圈外没有交集」。
- 子句：1. ¬P∨Q 2. ¬Q∨¬R 3. P∨¬R 4. R（否定结论）；5. P（3,4）→ 6. Q（1,5）→ 7. ¬R（2,6）→ 8. □（4,7）。⭐ 还要走第 8 步，是因为反证法要的不是「推出了 ¬R」，而是「假设 R 会导致矛盾」——终点必须是 □。
- CNF：1. ¬A∨B∨C 2. A 3. ¬B 4. ¬C（否定结论）。5. B∨C（1,2 消 A）→ 6. C（3,5 消 B）→ 7. □（4,6 消 C）✅。
- 反例：
P ⊨ P ∨ Q成立，但从子句P推不出P ∨ Q——分辨率只会消文字、不会加文字。⭐ 正因为它推不出任意公式、却一定能揪出矛盾（反驳完备），所以必须把「证 φ」翻译成「证 KB ∪ {¬φ} 不可满足」，让问题落到它的强项上。 - 本章的推理是保真的符号变形，⭐ 推出来的必然为真，失败方式是「推不出来 / 超时」；LLM 的思维链是生成一段看起来像推理的文本，没有任何保证，失败方式是推出错的东西而且理由写得很像样。所以常见做法是让模型做翻译、让求解器保正确。
🛑 可以停在这里
⚡ 走神救援
等价律：消去蕴含 φ→ψ ≡ ¬φ∨ψ、双重否定、德摩根、分配律、逆否——前几条把 ¬ 往里赶，分配律把 ∨ 往里赶。NNF = 否定只贴在字母前（手算过
¬(P ∨ (¬R ∧ P))≡¬P ∧ (R ∨ ¬P)）。文字 = 字母或其否定；子句 = 文字的析取；CNF = 子句的合取，⭐ 一个 CNF 就是一张约束清单（每个子句说「这几个文字至少有一个真」），所以常直接写成子句集合。⭐ 同时含L和¬L的子句恒真，直接扔（P ∨ (¬Q ∧ (R→¬P))靠这一招化到P ∨ ¬Q）。⚠️ 分配律会爆炸：(G∨H) → (¬J∧¬K)转出 4 个子句，m 个合取 ∨ n 个合取 → m×n 个。⭐⭐ 分辨率规则：α∨β与¬β∨γ推出α∨γ；可靠的理由一行——β 假则靠 α，β 真则靠 γ，两种情况α∨γ都真。三个面孔：推出空子句 □、蕴含的传递性、假言推理是它的特例。□ 代表假，因为「在零个文字里至少有一个为真」不可能。⭐⭐ 核心套路是反证法四步：否定结论 → 全转 CNF → 反复分辨 → 推出 □；它对，是因为 KB ⊨ φ ⟺ Mod(KB) ⊆ Mod(φ) ⟺ KB ∪ {¬φ} 不可满足（第 4 章的文氏图：小圈套在大圈里 ⟺ 小圈与大圈外无交集）。⭐ 为什么必须反证：分辨率只消文字不加文字，所以不完备（P ⊨ P∨Q却推不出P∨Q），但反驳完备——把问题翻译成「找矛盾」正好落在它强项上。完整例子：P→Q, Q→¬R, P∨¬R ⊢ ¬R，子句 ¬P∨Q / ¬Q∨¬R / P∨¬R / R，8 步推到 □；⚠️ 第 7 步已得到 ¬R，终点仍必须是 □。手算习惯：编号、单元优先。⚠️ 分辨率指数时间，剪枝四招：单元优先、删恒真子句、删被包含子句、删纯文字子句。落点：CNF + 反证就是 SAT 求解器。⚠️ LLM 的「推理」不是这个推理：本章的推理保真，失败是超时；思维链没有保证，失败是推出错的还写得很像样——所以常见组合是「模型做翻译、求解器保正确」。
下一节 👉 06-一阶逻辑.md ⭐⭐
去那里的理由：到这里为止，
P里面的「苏格拉底」和「秃头」一直是看不见的。 06 把它们找回来——同一套反证 + 分辨率，加上 Skolem 化和合一两个零件， 就能处理「所有人都会死」这种句子，顺便解开第 2 章那个积木谜题。