第 III 部分 · 知识、推理与规划
第 9 章 一阶逻辑中的推理
Chapter 9 · Inference in First-Order Logic
本章导读
把命题归结推广到一阶：合一处理变量绑定，前向 / 后向链在 Horn 子句上高效运行，归结反证提供通用但昂贵的完备推理。
学习要点
- 直接命题化的指数爆炸问题：一阶推理必须利用变量的结构性。
- 合一算法：求使两个文字一致的最一般合一子（MGU）；替换的合成。
- 前向链：数据驱动，与或图展开；规则库的效率优化与冗余事实问题。
- 后向链：目标驱动，Prolog 的执行模型；循环目标与重复子目标的处理。
- 一阶归结与反证：Skolem 化消去存在量词，归结反证的可靠性与完备性。
核心概念
| 术语 | English | 一句话解释 |
|---|---|---|
| 合一 | Unification | 求使两个逻辑表达式一致的变量替换 |
| 最一般合一子 | MGU | 约束最少的合一替换 |
| 前向链 | Forward Chaining | 从已知事实出发逐条触发规则 |
| 后向链 | Backward Chaining | 从目标出发逆向寻找支持事实 |
| Horn 子句 | Horn Clause | 至多含一个正文字的子句，链式推理的基础 |
| Skolem 化 | Skolemization | 用 Skolem 函数替换存在变量以消去 ∃ |
| 归结反证 | Resolution Refutation | 否定目标、推导空子句的证明方式 |
| 广义假言推理 | Generalized Modus Ponens | 带变量绑定的假言推理规则 |
| 与或图 | AND–OR Graph | 前向链展开形成的推理结构 |
配套代码（aima-python）
aima-python 是官方维护的开源算法库（MIT 协议），建议每学完一章就跑一遍对应模块的示例。