第 9 章聚焦于一阶逻辑的推理算法，旨在解决「如何自动判断一个语句是否为一阶逻辑知识库的逻辑推论」的问题。核心内容包括：

命题化（Propositionalization）

• 将一阶逻辑知识库转化为命题逻辑，然后使用命题推理算法（如 DPLL）
• 关键问题：需要实例化所有可能的常量项，可能无限；但 Herbrand 定理保证如果语句为真，则存在有限子集足以证明
• 完备性：存在完备的命题化方法（如扩展的完备定理），但实际中效率低

合一（Unification）

• 寻找两个逻辑表达式的最一般合一器（MGU），是实现高效推理的核心
• 常见合一算法（如递归遍历，带发生检查）

一阶归结（Resolution）

• 将公式转换为子句形式（CNF），应用归结规则，其中需要使用合一
• 范式转换：消去蕴含、否定内移、Skolem 化、变量标准化
• 完备性：一阶归结是完备的（如果语句不可满足，最终会归结出空子句）
• 归结策略（如归结完备性、支持集策略、线性归结、超归结等）用于提高效率

一阶前向链接

• 针对一阶霍恩子句（事实、规则）的推理算法
• 使用合一匹配规则前件，从已知事实推导新事实，直到不再变化（或达到目标）
• 应用：数据驱动推理、语义网、专家系统

一阶反向链接

• 目标驱动推理，从查询出发，递归匹配规则结论，生成子目标
• 基于合一实现规则匹配
• 逻辑编程语言（如 Prolog）的核心机制，采用深度优先搜索和回溯

逻辑编程

• 以 Prolog 为例，介绍其语法、执行模型（深度优先 + 合一 + 回溯）
• 控制谓词如 cut（!）用于剪枝
• 对比逻辑推导与程序设计

效率问题

• 前向链接可能生成大量无关事实，反向链接可能陷入无限递归
• 处理技巧：使用魔法集（MAGIC sets）变换，或者基于规则的散列等