Ch7-8 逻辑推理 (Logical Reasoning)

课件：lec7.pdf (117 页, 逻辑 Agent/命题逻辑) + lec8.pdf (91 页, 一阶逻辑/FOL 推理) + pl_fol.pdf (56 页, 命题与一阶逻辑补充)
教材：Artificial Intelligence: A Modern Approach (Russell & Norvig), Ch7 (Logical Agents) & Ch8 (First-Order Logic) & Ch9 (Inference in FOL)
教师：吉建民，USTC

0. 本章概述

本章是"知识、推理与规划"模块的开端，由命题逻辑与一阶逻辑两部分合并。逻辑是 1990 年代前 AI 的主导范式——它用形式化语言刻画知识，并借助保真 (truth-preserving) 的推理规则紧凑地导出新结论。命题逻辑以"事实 (facts)"为本体论约定，表达能力有限；一阶逻辑 (FOL) 引入对象、关系、函数与量词，表达能力大幅增强，但推理变为半可判定 (semidecidable)。后续章节的不确定性推理（贝叶斯网）与学习可视为对逻辑"确定性、难微调"两大缺点的回应。

第一部分：逻辑 Agent 与命题逻辑 (lec7)

1.1 动机：为什么需要逻辑？

三类建模范式

逻辑推理 (logical inference) 与模型检测 (model checking) 的区别：前者施加一组保真规则紧凑地推导（如由 $X_1+X_2=10,\ X_1-X_2=4$ 直接推 $X_1=7$）；后者直接枚举赋值验证。

逻辑的历史地位

• 1990 年代前是 AI 主导范式。
• 缺点 1：确定性 (deterministic)，不处理不确定性 → 概率论解决。
• 缺点 2：规则化，难从数据微调 → 机器学习解决。
• 优点：紧凑的表达能力 (expressivity)——尚未被概率/ML 完全取代。

两个目标：Elaboration Tolerance 与统一表示

• Elaboration Tolerance (McCarthy, 1998)：形式化应方便地修改以纳入新现象/新情况。
• 统一问题表示：问题实例 $I$ 表示为事实集 $P_I$，问题类 $C$ 表示为规则集 $P_C$，$P_C$ 可解 $C$ 中所有实例——即知识驱动软件 (knowledge-driven software)。

语言三层级

1.2 知识库 Agent (Knowledge-Based Agent)

⭐ 知识库 (Knowledge Base, KB)：关于世界知识的集合，每条知识对应一个语句 (sentence)，用某种知识表示语言 (knowledge representation language) 表达。

• 推理机 (Inference System)：根据 KB 推出隐含知识。例 $\text{KB}=\{\text{下雨},\ \text{下雨}\Rightarrow\text{地湿}\}$ ⟹ 推出"地湿"。

逻辑 Agent 操作循环：

1. TELL KB 新观察/新知识；
2. ASK KB 下一步采取什么行动；
3. 执行行动，并 TELL KB 结果。

Agent 三层次（pl_fol 补充）

KR 假设（Levesque 1986 引 Leibniz）

思维可理解作符号表示上的机械操作。如同算术有保值 (value-preserving) 演算，思想可有保真 (truth-preserving) 演算。

KR 根本问题：平衡表达能力 (expressiveness) 与推理效率 (tractability)。

1.3 Wumpus 世界 (Wumpus World)

PEAS 描述

环境表征

• Partially observable（仅局部感知当前格）、Deterministic、Sequential、Static、Discrete、Single-agent（Wumpus 实为自然特征）。

KB 推理示例

感知 breeze ⟹ 相邻方格可能有 pit；感知 stench ⟹ 相邻可能有 wumpus。据此标记安全方格并规划路径。（探索过程图示见原课件 lec7.pdf，需对照查看。）

1.4 逻辑的一般概念 (Ingredients of a Logic)

⭐ 一个逻辑由三要素构成：

核心关系

• 蕴涵 (Entailment)：$\text{KB}\models\alpha$ iff $\alpha$ 在所有 KB 为真的世界中为真 iff $M(\text{KB})\subseteq M(\alpha)$。
• 推理 (Inference)：$\text{KB}\vdash\alpha$ iff $\alpha$ 可由某过程从 KB 推出（派生 derived）。
• 可靠性 (Soundness)：若 $\text{KB}\vdash\alpha$ 则 $\text{KB}\models\alpha$（推出的都真）。
• 完备性 (Completeness)：若 $\text{KB}\models\alpha$ 则 $\text{KB}\vdash\alpha$（真的都能推出）。

逻辑谱系（表达能力递增）

Horn 命题逻辑 < 命题逻辑 < 模态逻辑 (Modal) < 一阶 Horn < 一阶逻辑 (FOL) < 二阶逻辑 < 非单调逻辑（Default / Autoepistemic / Circumscription / MKNF）。

本体论约定 (ontological commitment) 与认识论约定 (epistemological commitment) 对比（lec8）：

1.5 命题逻辑语法 (Propositional Logic Syntax)

• 命题符号 (Propositional symbols / 原子公式)：$A,B,C,\dots$
• 联结词 (Logical connectives)：$\lnot,\ \land,\ \lor,\ \to,\ \leftrightarrow$
• 递归构造：若 $f,g$ 是公式，则 $\lnot f,\ f\land g,\ f\lor g,\ f\to g,\ f\leftrightarrow g$ 也是公式。
• 公式本身只是符号（语法），尚无含义（语义）。

术语

形式系统 $L$（pl_fol，Hilbert 系统）

• 联结词 $\lnot,\to$ 为基本；$\land,\lor,\leftrightarrow$ 为辅助，定义为：
  • $p\land q\ =_{df}\ \lnot(p\to\lnot q)$
  • $p\lor q\ =_{df}\ \lnot p\to q$
  • $p\leftrightarrow q\ =_{df}\ \lnot((p\to q)\to\lnot(q\to p))$
• 公理模式：
  • (L1) $p\to(q\to p)$
  • (L2) $(p\to(q\to r))\to((p\to q)\to(p\to r))$
  • (L3) $(\lnot p\to\lnot q)\to(q\to p)$
• 推理规则 (MP)：从 $p,\ p\to q$ 推出 $q$。

形式证明与推导（pl_fol）

• 形式证明：$p$ 的序列 $p_1,\dots,p_n=p$，每步是公理或由前序 $p_i,p_j(=p_i\to p_k)$ 经 MP。记 $\vdash p$（$p$ 是 $L$ 的内定理）。
• 形式推导（从 $\Gamma$）：每步是公理、或属于 $\Gamma$、或经 MP。记 $\Gamma\vdash p$。

1.6 命题逻辑语义 (Semantics)

⭐ 模型 (Model)：$w$ 是对命题符号的真值赋值。$n$ 个命题符号 ⟹ $2^n$ 个模型。

⭐ 解释函数 (Interpretation function) $I(f,w)\in\{\text{true}(1),\text{false}(0)\}$：

• 基例：$I(p,w)=w(p)$。
• 递归：
  • $I(\lnot f,w)=\lnot I(f,w)$
  • $I(f\land g,w)=I(f,w)\land I(g,w)$
  • $I(f\lor g,w)=I(f,w)\lor I(g,w)$
  • $I(f\to g,w)=\lnot I(f,w)\lor I(g,w)$
  • $I(f\leftrightarrow g,w)=(I(f,w)\leftrightarrow I(g,w))$

⭐ $M(f)=\{w\mid I(f,w)=1\}$：公式 $f$ 满足的模型集。

⭐ 知识库：$M(\text{KB})=\bigcap_{f\in\text{KB}} M(f)$（合取 / 交）。直觉：KB 给世界施加约束，$M(\text{KB})$ 是满足约束的所有世界。

1.7 核心语义关系

命题：KB contradicts $f$ iff $\text{KB}\models\lnot f$。

⭐ 核心等价（贯穿全章）：

$$\boxed{\ \text{KB}\models f\ \iff\ \text{KB}\land\lnot f\ \text{不可满足}\ }$$

• TELL：把新句加入 KB；ASK：查询是否蕴涵某句。

1.8 有效性与可满足（pl_fol 补充）

• 有效 (valid)：所有模型为真。重言式 (tautology)，如 $p\to p,\ (\lnot p\to p)\to p$。
• 可满足 (satisfiable)：某些模型为真。
• 不可满足 (unsatisfiable)：无模型为真。永假式 (contradiction)，如 $p\land\lnot p$。
• $p$ 有效 iff $\lnot p$ 不可满足。

复杂性（pl_fol）

• 判定 $\text{KB}\models p$：coNP-complete。
• 判定 $p$（或 $\text{KB}\land\lnot p$）可满足：NP-complete。

可靠性与完备性

• $\vdash$ 可靠：$\Gamma\vdash p\Rightarrow\Gamma\models p$。
• $\vdash$ 完备：$\Gamma\models p\Rightarrow\Gamma\vdash p$。

1.9 逻辑等值律 (Logical Equivalences) ⭐⭐⭐

若 $\models p\leftrightarrow q$，则 $p$ 与 $q$ 逻辑等值。等值替换规则：若 $\models q\leftrightarrow q'$，则在 $p$ 中用 $q'$ 替换子公式 $q$ 得 $p'$，则 $\models p\leftrightarrow p'$。

1.10 合取范式 (CNF / DNF)

转 CNF 三步

1. 消去 $\to$ 和 $\leftrightarrow$（用蕴含消去 + 双条件消去）；
2. $\lnot$ 深入（用 De Morgan + 双否消去）；
3. 对 $\land$ 和 $\lor$ 分配整理。

例：$(x_1\land(x_2\to x_3))\to x_2$

• 消 $\to$：$\lnot(x_1\land(\lnot x_2\lor x_3))\lor x_2$
• $\lnot$ 深入：$(\lnot x_1\lor(x_2\land\lnot x_3))\lor x_2$
• 分配律：$(\lnot x_1\lor x_2)\land(\lnot x_1\lor x_2\lor\lnot x_3)$

1.11 模型检测 (Model Checking)

SAT（可满足性）= CSP 的特例（变量=命题符号，域 $\{T,F\}$，约束=子句）。

1.12 推理规则与证明方法

Modus Ponens (MP)

$$\frac{p,\quad p\to q}{q}$$

推理规则一般式：$\dfrac{f_1,\dots,f_k}{g}$。派生 (Derivation)：$\text{KB}\vdash f$ iff $f$ 最终加入 KB。

期望性质 (Desiderata)

可靠 (sound)、完备 (complete)、高效 (efficient)。

证明方法两大类

1. 推理规则应用：证明=推理规则应用序列；可作搜索问题（后继函数=规则所有可能应用）；常需转正规形式。
2. 模型检测：真值表枚举 $O(2^n)$；改进回溯 DPLL；启发式搜索（可靠但不完备，如 min-conflicts 爬山）。

1.13 Horn 子句与确定子句 ⭐

⭐ 确定子句 (Definite clause)：$(p_1\land\dots\land p_k)\to q$，其中 $p_i$（$k\ge 0$）与 $q$ 是命题符号。

• 例：$(\text{Rain}\land\text{Snow})\to\text{Traffic}$；$\text{Traffic}$（$k=0$）。
• 非例：$\text{Rain}\land\text{Snow}$（非蕴涵）、$\lnot\text{Traffic}$（含否定）、$(\text{Rain}\land\text{Snow})\to(\text{Traffic}\lor\text{Peaceful})$（结论为析取）。

⭐ Horn 子句 (Horn clause)：确定子句 或 目标子句 $(p_1\land\dots\land p_k)\to\bot$（等价 $\lnot(p_1\land\dots\land p_k)$）。

Modus Ponens on Horn clauses

$$\frac{p_1,\dots,p_k,\quad (p_1\land\dots\land p_k)\to q}{q}$$

⭐ 定理（Horn 上完备）：若 KB 只含 Horn 子句且 $p$ 是被蕴涵的命题符号，则 MP 必能推出 $p$。即

$$\text{KB}\models p\ \iff\ \text{KB}\vdash p$$

• MP 仅能生成命题符号（非否定），故只能答 “yes” 或 “I don’t know”——因为全真赋值恒为模型，永不答 “no”。

1.14 前向链与反向链 ⭐⭐⭐

前向链 (Forward Chaining)

• 数据驱动：从已知事实出发，反复触发前提已满足的确定子句，加入新结论，直到无新事实或得到查询。
• 性质（Horn KB）：
  • 可靠：每次推理本质是 MP 的一次应用。
  • 完备：每个被蕴含的原子语句终被生成。
  • 线性时间。
• 完备性证明思路：设最小模型（所有可推出原子为真），任何被蕴含原子必在其中。

反向链 (Backward Chaining)

• 目标驱动：从查询目标出发，反向找以该目标为头的规则，递归证明其前提。

前向 vs 反向

1.15 命题归结 (Resolution) ⭐⭐⭐

⭐ 归结规则：

• Unit Resolution：$\dfrac{\alpha\lor\beta,\quad \lnot\beta}{\alpha}$
• General Resolution：$\dfrac{\alpha\lor\beta,\quad \lnot\beta\lor\gamma}{\alpha\lor\gamma}$

归结算法

1. 将公式化为子句集合（CNF）；
2. 反复使用归结规则；
3. 无可添加新子句 ⟹ 可满足；出现空子句 $\square$ ⟹ 不可满足。

⭐ 归结反演：证明 $\text{KB}\models p$ ⟺ 证明 $\text{KB}\land\lnot p$ 不可满足 ⟺ 转 CNF 后归结出空子句。

• 命题逻辑中归结算法可靠、完备。
• 时间复杂度：指数级（子句数与归结步数）。

第二部分：一阶逻辑 (First-Order Logic, lec8)

2.1 为何需要 FOL？

命题逻辑的优缺点

优点：

• 陈述性 (declarative)：知识与推理分离，且推理完全不依赖领域（对比程序设计语言的过程性）。
• 支持部分/析取/否定信息（不像大多数数据库）。
• 组合性 (compositional)：复合句含义是各部分含义的函数。
• 上下文无关 (context-independent)（不像自然语言）。

缺点：表达力弱。不能说"陷阱在相邻方格引起微风"，只能逐格写 $B_{1,1}\leftrightarrow(P_{1,2}\lor P_{2,1})$。缺对象/关系与量词/变量。

FOL 的本体论约定

命题逻辑假设世界含事实 (facts)；一阶逻辑（如自然语言）假设世界含：

• 对象 (Objects)：人、房屋、数、颜色、棒球赛、战争…
• 关系 (Relations)：red、round、prime；brother of、bigger than、part of…
• 函数 (Functions)：father of、best friend、one more than、plus…

谓词描述个体（可独立存在事物）间的关系或属性。

2.2 FOL 语法 (Syntax)

⭐ 基本元素：

⭐ 项 (Term) $=$ 函数(项$_1,\dots,$项$_n$) 或 常量 或 变量。

⭐ 原子句 (Atomic sentence) $=$ 谓词(项$_1,\dots,$项$_n$) 或 项$_1=$项$_2$。

• 例：$\text{Brother}(\text{KingJohn},\text{Richard})$；$>(\text{Length}(\text{LeftLegOf}(\text{Richard})),\text{Length}(\text{LeftLegOf}(\text{KingJohn})))$。

⭐ 复合句 (Complex sentence)：用联结词连接原子句。例 $\text{Sibling}(\text{KingJohn},\text{Richard})\Rightarrow\text{Sibling}(\text{Richard},\text{KingJohn})$。

形式系统 $K$（pl_fol）

符号表：

• 逻辑符号：个体变元 $x_1,x_2,\dots$；联结词 $\lnot,\to,\land,\lor,\leftrightarrow$；量词 $\forall,\exists$。
• 非逻辑符号：个体常元 $a_1,a_2,\dots$；函项符号 $f_{n,m}$（按元数）；谓词符号 $P_{n,m}$。

形成规则：

• 项：(1) 变元/常元是项；(2) $f$ 是 $n$ 元函项符号，$t_i$ 是项 ⟹ $f(t_1,\dots,t_n)$ 是项。
• 公式：(1) $P$ 是 $n$ 元谓词，$t_i$ 项 ⟹ $P(t_1,\dots,t_n)$ 原子公式；(2) $\lnot p, p\to q, p\land q, p\lor q, p\leftrightarrow q$ 复合公式；(3) $\forall x\,p,\ \exists x\,p$ 量化公式。

术语（pl_fol）

• 子公式；自由/约束出现（$\forall x\,p$ 中 $x$ 约束，$p$ 为辖域）；闭项/开项（不含/含变元）；闭公式/开公式（无/有自由变元）；项 $t$ 对 $p(x)$ 中 $x$ 自由（替换后 $t$ 中变元仍自由）。

公理系统 $K$

• (K1) $p\to(q\to p)$
• (K2) $(p\to(q\to r))\to((p\to q)\to(p\to r))$
• (K3) $(\lnot p\to\lnot q)\to(q\to p)$
• (K4) $\forall x\,p(x)\to p(t)$（项 $t$ 对 $p(x)$ 中 $x$ 自由）
• (K5) $\forall x(p\to q)\to(p\to\forall x\,q)$（$x$ 不在 $p$ 自由出现）
• 推理规则：(MP) $p,p\to q\vdash q$；(UG, Universal Generalization) $p\vdash\forall x\,p$。

2.3 FOL 语义 (Semantics)

⭐ 语句真值由一个模型 (model) 和解释 (interpretation) 判定。

• 模型含对象（域元素 domain elements）及其间关系。
• 解释指定指代 (referents)：
  • 常量符号 ⟶ 对象
  • 谓词符号 ⟶ 关系
  • 函数符号 ⟶ 函数关系
• 原子句 $\text{predicate}(t_1,\dots,t_n)$ 为真 iff $t_i$ 指代的对象处于 predicate 指代的关系中。

形式语义（pl_fol）

• 一阶结构 $M=(D,F,P)$：论域 $D$（非空）；$D$ 上函数集 $F$；$D$ 上关系集 $P$。
  • 常元 $a\mapsto a^M\in D$；$n$ 元函数符号 $\mapsto f^M:D^n\to D$；$n$ 元谓词 $\mapsto P^M\subseteq D^n$。
• 个体变元指派 $V:Y\to D$；一阶解释 $I=(M,V)$。
• 赋值：
  • $I(x)=V(x)$；$I(f(t_1,\dots,t_n))=f^M(I(t_1),\dots,I(t_n))$。
  • $P(t_1,\dots,t_n)$ 真 iff $(I(t_1),\dots,I(t_n))\in P^M$。
  • $\forall x\,p$ 真 iff 对所有 $d\in D$，$I_{x=d}(p)$ 真。
  • $\exists x\,p$ 真 iff $\lnot\forall x\,\lnot p$ 真。
  • $I_{x=d}=(M,V|_{x=d})$，$V|_{x=d}(y)=\begin{cases}d&y=x\\V(y)&\text{otherwise}\end{cases}$。

模型与有效性（pl_fol）

• $M$ 有效：对一切 $V$，$p$ 在 $(M,V)$ 真 ⟹ $M\models p$。
• 逻辑有效：对一切结构 $M$，$M\models p$，记 $\models p$。
• 模型：$M\models\Gamma$（对 $\Gamma$ 中所有 $p$，$M\models p$）。
• 语义后承 $\Gamma\models p$：对一切 $M$，$M\models\Gamma\Rightarrow M\models p$。
• FOL 公理系统与语义可靠、完备。

FOL 模型无穷多

枚举 FOL 模型不可行：域个数 $n:1\to\infty$ → 每个 $k$ 元谓词的关系 → 每个常量指代… ⟹ 通过枚举模型检验蕴涵不可行。

FOL 的局限（pl_fol）

无法刻画极小、传递闭包等关系（如仅靠 parent 公理无法定义 ancestor 传递闭包，需归纳/不动点）。

2.4 量词 (Quantifiers) ⭐⭐⭐

全称量词 (Universal) $\forall$

$$\forall x\ \text{At}(x,\text{USTC})\Rightarrow\text{Smart}(x)$$

• “$\forall x\,P$” 在模型 $m$ 中为真 iff 对每个对象 $x$，$P$ 为真。≈ 实例的合取式。

⚠️ 常见错误：$\forall$ 与 $\land$ 搭配——$\forall x\,\text{At}(x,\text{USTC})\land\text{Smart}(x)$ 意为"所有人都在 USTC 且都聪明"。正确：$\forall$ 配 $\Rightarrow$。

存在量词 (Existential) $\exists$

$$\exists x\ \text{At}(x,\text{USTC})\land\text{Smart}(x)$$

• “$\exists x\,P$” 真 iff $P$ 对某对象为真。≈ 实例的析取式。

⚠️ 常见错误：$\exists$ 与 $\Rightarrow$ 搭配——$\exists x\,\text{At}(x,\text{USTC})\Rightarrow\text{Smart}(x)$，只要有人不在 USTC 即真！正确：$\exists$ 配 $\land$。

量词性质

• $\forall x\forall y = \forall y\forall x$；$\exists x\exists y = \exists y\exists x$。
• 但 $\exists x\forall y \neq \forall y\exists x$：
  • $\exists x\forall y\,\text{Loves}(x,y)$：“存在一人爱所有人”。
  • $\forall y\exists x\,\text{Loves}(x,y)$：“每人被至少一人爱”。

⭐ 量词对偶 (Duality)：

$$\forall x\,P \equiv \lnot\exists x\,\lnot P\qquad \exists x\,P \equiv \lnot\forall x\,\lnot P$$

等词 (Equality)

$\text{term}_1=\text{term}_2$ 为真 iff 指代同一对象。

Sibling 定义：

$$\forall x,y\ \text{Sibling}(x,y)\Leftrightarrow\big[\lnot(x=y)\land\exists m,f\ \lnot(m=f)\land\text{Parent}(m,x)\land\text{Parent}(f,x)\land\text{Parent}(m,y)\land\text{Parent}(f,y)\big]$$

2.5 使用 FOL：领域建模

亲属域 (Kinship)

• $\forall x,y\ \text{Brother}(x,y)\Rightarrow\text{Sibling}(x,y)$
• Sibling 对称：$\forall x,y\ \text{Sibling}(x,y)\Rightarrow\text{Sibling}(y,x)$
• $\forall x,y\ \text{Mother}(x,y)\Leftrightarrow(\text{Female}(x)\land\text{Parent}(x,y))$
• $\forall x,y\ \text{Cousin}(x,y)\Leftrightarrow\exists p,ps\ \text{Parent}(p,x)\land\text{Sibling}(ps,p)\land\text{Parent}(ps,y)$

集合域 (Set)

• $\forall s\ \text{Set}(s)\Leftrightarrow(s=\{\})\lor(\exists x,s_2\ \text{Set}(s_2)\land s=\{x|s_2\})$
• 空集不可分解：$\lnot\exists x,s\ \{x|s\}=\{\}$
• 子集：$\forall s_1,s_2\ s_1\subseteq s_2\Leftrightarrow(\forall x\ x\in s_1\Rightarrow x\in s_2)$
• 相等：$\forall s_1,s_2\ (s_1=s_2)\Leftrightarrow(s_1\subseteq s_2\land s_2\subseteq s_1)$
• 交：$\forall x,s_1,s_2\ x\in(s_1\cap s_2)\Leftrightarrow(x\in s_1\land x\in s_2)$
• 并：$\forall x,s_1,s_2\ x\in(s_1\cup s_2)\Leftrightarrow(x\in s_1\lor x\in s_2)$

Wumpus 域 FOL KB

• 感知：$\forall t,s,b\ \text{Percept}([s,b,\text{Glitter}],t)\Rightarrow\text{Glitter}(t)$
• 反射：$\forall t\ \text{Glitter}(t)\Rightarrow\text{BestAction}(\text{Grab},t)$
• 带内部状态：$\forall t\ \text{AtGold}(t)\land\lnot\text{Holding}(\text{Gold},t)\Rightarrow\text{BestAction}(\text{Grab},t)$

⭐ 诊断规则 (Diagnostic) vs 因果规则 (Causal)：

• 诊断（由果推因）：$\forall s\ \text{Breezy}(s)\Rightarrow\exists r\ \text{Adjacent}(r,s)\land\text{Pit}(r)$

• 因果（由因推果）：$\forall r,s\ \text{Adjacent}(r,s)\land\text{Pit}(r)\Rightarrow\text{Breezy}(s)$

• Breezy 定义：$\forall s\ \text{Breezy}(s)\Leftrightarrow\exists r\ \text{Adjacent}(r,s)\land\text{Pit}(r)$

• Adjacent：$\forall x,y,a,b\ \text{Adjacent}([x,y],[a,b])\Leftrightarrow[a,b]\in\{[x+1,y],[x-1,y],[x,y+1],[x,y-1]\}$

与 FOL KB 交互（置换/substitution）

• $\text{Tell}(\text{KB},\text{Percept}([\text{Smell},\text{Breeze},\text{None}],5))$
• $\text{Ask}(\text{KB},a\ \text{BestAction}(a,5))$ ⟹ 答 $\{a/\text{Shoot}\}$（绑定表 binding list）。
• 给定句子 $S$ 与置换 $\sigma$，$S\sigma$ 为代入结果。$\text{Ask}(\text{KB},S)$ 返回部分/所有使 $\text{KB}\models S\sigma$ 的 $\sigma$。

2.6 知识工程 (Knowledge Engineering) 七步

1. 确定任务 (Identify the task)。
2. 搜集相关知识 (Assemble relevant knowledge)。
3. 确定词汇表 (vocabulary)：谓词/函数/常量。
4. 编码通用域知识 (Encode general knowledge)。
5. 编码特定问题实例 (Encode specific instance)。
6. 提交查询获取答案 (Pose queries)。
7. 调试 KB (Debug)。

电路域 (Electronic Circuits) 例——一位全加器

• 任务：电路验证（是否正确相加）。
• 相关知识：由导线 (wires) 和门 (gates) 组成；门类型 AND/OR/XOR/NOT；忽略大小/形状/颜色。
• 词汇表：$\text{Type}(X_1)=\text{XOR}$ 或 $\text{Type}(X_1,\text{XOR})$ 或 $\text{XOR}(X_1)$。
• 通用知识公理：
  • $\forall t_1,t_2\ \text{Connected}(t_1,t_2)\Rightarrow\text{Signal}(t_1)=\text{Signal}(t_2)$
  • $\forall t\ \text{Signal}(t)=1\lor\text{Signal}(t)=0$；$1\neq 0$
  • Connected 可交换：$\forall t_1,t_2\ \text{Connected}(t_1,t_2)\Rightarrow\text{Connected}(t_2,t_1)$
  • OR 门：$\forall g\ \text{Type}(g)=\text{OR}\Rightarrow\text{Signal}(\text{Out}(1,g))=1\Leftrightarrow\exists n\ \text{Signal}(\text{In}(n,g))=1$
  • AND 门：输出 0 iff 某 输入 0
  • XOR 门：输出 1 iff 两输入不同
  • NOT 门：输出与输入相反
• 查询：$\exists i_1,i_2,i_3,o_1,o_2\ \text{Signal}(\text{In}(1,C_1))=i_1\land\dots\land\text{Signal}(\text{Out}(2,C_1))=o_2$。
• 调试：可能遗漏 $1\neq 0$ 等断言。

第三部分：FOL 推理 (Inference in FOL)

3.1 命题化 (Reduction to Propositional Inference)

⭐ 全称实例化 (UI, Universal Instantiation)：

$$\frac{\forall v\ \alpha}{\text{Subst}(\{v/g\},\alpha)}$$

对任意变量 $v$ 和基项 (ground term) $g$。

• 例 $\forall x\ \text{King}(x)\land\text{Greedy}(x)\Rightarrow\text{Evil}(x)$ 得 $\text{King}(\text{John})\land\text{Greedy}(\text{John})\Rightarrow\text{Evil}(\text{John})$ 等。
• UI 可多次应用；新 KB 与旧 KB 逻辑等价。

⭐ 存在实例化 (EI, Existential Instantiation)：

$$\frac{\exists v\ \alpha}{\text{Subst}(\{v/k\},\alpha)}$$

$k$ 为不出现在 KB 他处的新常量符号，称 Skolem 常数 (Skolem constant)。

• 例 $\exists x\ \text{Crown}(x)\land\text{OnHead}(x,\text{John})$ ⟹ $\text{Crown}(C_1)\land\text{OnHead}(C_1,\text{John})$。
• EI 只能应用一次；新 KB 不等价于旧 KB，但可满足性等价（satisfiable iff）。

命题化与 Herbrand 定理

命题化 KB 与查询，应用归结，返回结果。

⚠️ 问题：有函数符号时基项无穷（如 $\text{Father}(\text{Father}(\text{Father}(\text{John})))$）。

⭐ Herbrand 定理 (1930)：若语句 $\alpha$ 被 FOL KB 蕴涵，则存在仅涉及命题化 KB 有限子集的证明。

• 算法：$n=0\to\infty$，用深度 $n$ 项命题化，查是否蕴涵。
• 问题：$\alpha$ 被蕴涵则停；不被蕴涵则死循环。

⭐ 半可判定 (Semidecidable)（Turing 1936, Church 1936）：FOL 蕴涵半可判定——存在算法对每个被蕴涵语句答 yes，但不存在算法对每个非蕴涵语句答 no。

命题化的问题

• 生成大量无关语句（如 $\text{Greedy}(\text{Richard})$ 与结论无关）。
• $p$ 个 $k$ 元谓词 + $n$ 常量 ⟹ $p\cdot n^k$ 实例；有函数符号更糟。

3.2 合一 (Unification) ⭐⭐⭐

⭐ 若存在置换 $\theta$ 使 $\alpha\theta=\beta\theta$，则 $\theta$ 合一 $\alpha,\beta$，记 $\text{Unify}(\alpha,\beta)=\theta$。
示例（$\text{Knows}(\text{John},x)$ 与）：

⭐ 标准化分离 (Standardizing apart)：换名消除变量重叠，如 $\text{Knows}(z_{17},\text{OJ})$。

⭐ 最一般合一 (MGU)：对变量限制最少的合一者；对每个表达式对，MGU 唯一（至变量换名）。

• 例 $\text{Knows}(\text{John},x)$ 与 $\text{Knows}(y,z)$，MGU $=\{y/\text{John},x/z\}$（比 $\{y/\text{John},x/\text{John},z/\text{John}\}$ 更一般）。

置换与合成（pl_fol 形式定义）

• 置换 (substitution) $\theta=\{v_1/t_1,\dots,v_n/t_n\}$：$v_i$ 变量，$t_i\neq v_i$ 的项，$v_i\neq v_j$。
• $E\theta$：同时替换 $E$ 中所有 $v_i$ 为 $t_i$。
  • 例 $E=P(x,y,f(a))$，$\theta=\{x/b,y/x\}$ ⟹ $E\theta=P(b,x,f(a))$。
• 合成 $\theta\sigma$：先用 $\theta$ 再用 $\sigma$。
  • $\theta=\{x/f(y),y/z\}$，$\sigma=\{x/a,y/b,z/y\}$ ⟹ $\theta\sigma=\{x/f(b),z/y\}$。

合一者与 MGU（pl_fol）

• 合一者 (unifier) $\theta$：$S_1\theta=\dots=S_k\theta$。例 $\{P(f(x),z),P(y,a)\}$ 合一者 $\sigma=\{y/f(a),x/a,z/a\}$。
• mgu：对任意合一 $\sigma$ 存在 $\gamma$ 使 $\sigma=\theta\gamma$。例 mgu $=\{y/f(x),z/a\}$，$\sigma=\theta\{x/a\}$。
• mgu（等价）唯一。
• 分歧集 (disagreement set)：最左符号分歧处抽取的子表达式集合。例 $S=\{P(f(x),h(y),a),P(f(x),z,a),P(f(x),h(y),b)\}$ ⟹ $\{h(y),z\}$。
• 合一算法：$\sigma_0=\epsilon$；若 $\sigma_k$ 是 $S$ 合一则停（$\sigma_k$ 为 mgu）；否则找 $S\sigma_k$ 分歧集 $D_k$；若 $D_k$ 含变量 $v$ 与不含 $v$ 的项 $t$，$\sigma_{k+1}=\sigma_k\{v/t\}$；否则不可合一。

3.3 广义假言推理 (Generalized Modus Ponens, GMP) ⭐⭐⭐

⭐ GMP：

$$\frac{p'_1,p'_2,\dots,p'_n,\quad (p_1\land p_2\land\dots\land p_n\Rightarrow q)}{q\theta}$$

其中 $p'_i\theta=p_i\theta$ 对所有 $i$。
例：

• 用于确定子句 (definite clauses) KB（恰一个正文字）；所有变量默认全称量化。

半可判定

FOL（即使限制 Horn 子句）半可判定：若 KB 蕴涵 $f$，存在算法有限步证明；若不蕴涵，无算法有限步显示。

GMP 可靠性证明

需证 $p'_1,\dots,p'_n,(p_1\land\dots\land p_n\Rightarrow q)\models q\theta$（给定 $p'_i\theta=p_i\theta$）。

• 引理：对任意 $p$，$p\models p\theta$。

1. $(p_1\land\dots\land p_n\Rightarrow q)\models(p_1\land\dots\land p_n\Rightarrow q)\theta=(p_1\theta\land\dots\land p_n\theta\Rightarrow q\theta)$
2. $p'_1,\dots,p'_n\models p'_1\land\dots\land p'_n\models p'_1\theta\land\dots\land p'_n\theta$
3. 由 1、2 经普通 MP 得 $q\theta$。

GMP 完备性

• 对一般 FOL 不完备（非每句可转 Horn 形式）。
• 对确定子句 FOL KB 完备。

3.4 FOL 前向链 (Forward Chaining)

经典例：West 犯罪 KB

1
2
3
4
5
6
7

American(x) ∧ Weapon(y) ∧ Sells(x,y,z) ∧ Hostile(z) ⇒ Criminal(x)
Owns(Nono,M1), Missile(M1)        (由 ∃ 实例化)
Missile(x) ∧ Owns(Nono,x) ⇒ Sells(West,x,Nono)
Missile(x) ⇒ Weapon(x)
Enemy(x,America) ⇒ Hostile(x)
American(West)
Enemy(Nono,America)

前向链推导 ⟹ $\text{Criminal}(\text{West})$。

性质

• 对一阶确定子句可靠且完备（证明类似命题逻辑）。
• Datalog = 一阶确定子句 + 无函数（如犯罪 KB）⟹ FC 多项式迭代终止（至多 $p\cdot n^k$ 文字）。
• 一般情况 $\alpha$ 不被蕴涵时可能不终止（不可避免，因确定子句蕴涵半可判定）。

效率

• 无需在迭代 $k$ 重新匹配前提未在 $k-1$ 新增的规则。
• DB 索引允许 $O(1)$ 检索已知事实（如查 $\text{Missile}(x)$ 检索 $\text{Missile}(M_1)$）。
• 匹配合取前提与已知事实是 NP-hard。

3.5 FOL 反向链 (Backward Chaining)

• 深度优先递归证明搜索：空间线性于证明大小。

• 不完备（无限循环）⟹ 检查当前目标是否在栈中。

• 低效（重复子目标）⟹ 缓存先前结果（额外空间）。

• 广泛用于逻辑程序设计 (logic programming)（如 Prolog）。

• FC/BC 对 Horn KB 完备，但对一般 FOL 不完备。

3.6 前束范式 (Prenex Normal Form)（pl_fol）

形式 $Q_1 x_1\cdots Q_n x_n\,p$，$p$ 无量词（母式 matrix）。

转换规则（$Q^*$ 为 $Q$ 对偶量词）：

1. 改名：$|= Qx\,p(x)\leftrightarrow Qy\,p(y)$（条件）。
2. 移量词：$x$ 不在 $p$ 自由 ⟹ $|=(p\to Qx\,q)\leftrightarrow Qx(p\to q)$；$x$ 不在 $q$ 自由 ⟹ $|=(Qx\,p\to q)\leftrightarrow Q^*x(p\to q)$。
3. $\lnot$ 内移：$|=\lnot Qx\,p\leftrightarrow Q^*x\,\lnot p$。
4. $|=(\forall x\,p\land\forall x\,q)\leftrightarrow\forall x(p\land q)$。
5. $|=(\exists x\,p\lor\exists x\,q)\leftrightarrow\exists x(p\lor q)$。
6. $x$ 不在 $p$ 自由 ⟹ $|=(p\lor\forall x\,q)\leftrightarrow\forall x(p\lor q)$，$|=(p\land\exists x\,q)\leftrightarrow\exists x(p\land q)$。

3.7 FOL 转 CNF ⭐⭐⭐

⭐ 六步（示例"爱所有动物者被某人爱" $\forall x[\forall y\,\text{Animal}(y)\Rightarrow\text{Loves}(x,y)]\Rightarrow[\exists y\,\text{Loves}(y,x)]$）：

1. 消等价/蕴含 (Eliminate $\leftrightarrow,\Rightarrow$)：
   $\forall x[\lnot\forall y\,\lnot\text{Animal}(y)\lor\text{Loves}(x,y)]\lor[\exists y\,\text{Loves}(y,x)]$
2. $\lnot$ 内移 (Move $\lnot$ inwards)：$\lnot\forall x\,p\equiv\exists x\,\lnot p$，$\lnot\exists x\,p\equiv\forall x\,\lnot p$
   $\forall x[\exists y\,\text{Animal}(y)\land\lnot\text{Loves}(x,y)]\lor[\exists y\,\text{Loves}(y,x)]$
3. 变量标准化 (Standardize variables)：各量词不同变量
   $\forall x[\exists y\,\text{Animal}(y)\land\lnot\text{Loves}(x,y)]\lor[\exists z\,\text{Loves}(z,x)]$
4. Skolem 化 (Skolemize)：存在变量 ⟹ 所辖全称变量的 Skolem 函数
   $\forall x[\text{Animal}(F(x))\land\lnot\text{Loves}(x,F(x))]\lor\text{Loves}(G(x),x)$
5. 去全称量词 (Drop universal quantifiers)：
   $[\text{Animal}(F(x))\land\lnot\text{Loves}(x,F(x))]\lor\text{Loves}(G(x),x)$
6. $\lor$ 分配到 $\land$ (Distribute $\lor$ over $\land$)：
   $[\text{Animal}(F(x))\lor\text{Loves}(G(x),x)]\land[\lnot\text{Loves}(x,F(x))\lor\text{Loves}(G(x),x)]$