第07章 逻辑智能体

摘要：本章系统介绍了基于知识的智能体（Knowledge-Based Agent）及其核心推理机制——命题逻辑。首先阐述了逻辑智能体的基本架构（TELL/ASK接口）和Wumpus World经典环境，然后深入讲解了命题逻辑的语法、语义及关键概念（蕴涵、可靠性、完备性）。核心算法部分涵盖了模型检验（TT-ENTAILS）、归结（Resolution）、前向/后向链接、DPLL SAT求解器和WalkSAT局部搜索，并通过Wumpus World实战展示了命题逻辑智能体的构建。最后讨论了命题逻辑的表达局限，引出后续一阶逻辑的必要性，并探讨了逻辑智能体与现代AI（大语言模型、AI对齐、多模态感知）的关联与张力。

对应 Artificial Intelligence: A Modern Approach, 4th Edition 第 7 章 Logical Agents

---

1. 章节概述

本章是全书从"搜索式问题求解"转向"基于知识的问题求解"（knowledge-based problem solving）的分水岭。

前六章的智能体（搜索智能体、博弈智能体、CSP 智能体）都属于原子表示（atomic representation）或因子化表示（factored representation）的浅层使用：状态被当作黑盒或属性向量，智能体的"聪明"完全体现在搜索策略上。本章提出一种根本不同的路线：

让智能体拥有一个知识库（Knowledge Base, KB），用形式化的表示语言（representation language）描述世界，并通过逻辑推理（inference）从已知事实推导出新事实，进而决策。

这种做法的核心优势是部分可观测环境下的推理能力与知识的可组合复用：搜索智能体必须为每个具体任务重新设计状态与转移；而知识型智能体只需往 KB 里添加句子（TELL），推理机制（ASK）自动组合已有知识产生新结论。这是"知识与推理分离"（knowledge/inference separation）的工程价值，也是声明式（declarative）系统区别于过程式（procedural）系统的关键。

本章的主要线索：

1. 基于知识的智能体架构：TELL / ASK 接口与智能体主循环。
2. Wumpus World：一个经典的部分可观测、确定性、离散环境，用于展示"感知 → 推理 → 行动"的完整链条。
3. 逻辑的通用概念：语法（syntax）、语义（semantics）、模型（model）、蕴涵（entailment）、可满足性（satisfiability）、可靠性（soundness）与完备性（completeness）。
4. 命题逻辑（propositional logic）：最简单的完整逻辑，语法与语义规则、真值表。
5. 定理证明（theorem proving）：归结（resolution）、合取范式（CNF）、Horn 子句与前向/后向链接、DPLL、WalkSAT。
6. 命题逻辑的局限：无法简洁表达"所有"、“存在”，导致 Wumpus World 的知识库随格子数平方/立方膨胀 → 引出第 8 章一阶逻辑。
7. SATPlan：把规划问题编译为 SAT 问题求解，展示"逻辑作为通用求解基底"的威力。

读者应带走的核心直觉：逻辑蕴涵是一种"语义上的必然"，而推理算法是"语法上的操作"；一个好的推理算法要既可靠（不推出错的）又完备（能推出所有对的）。

---

2. 关键概念与定义

2.1 基于知识的智能体（Knowledge-Based Agent）

组件	说明
知识库 KB	一组句子（sentence）的集合，句子用知识表示语言书写，断言关于世界的事实
公理（axiom）	不由其他句子推导得来、直接给定的句子
TELL	向 KB 添加新句子的操作
ASK	向 KB 查询的操作，返回"KB 是否蕴涵某句子"，或返回满足查询的绑定
推理（inference）	从旧句子导出新句子的过程；要求导出的句子必须是 KB 的逻辑推论（logical consequence）

标准智能体主循环：

function KB-AGENT(percept) returns an action
    persistent: KB, 知识库
                t, 计数器，初值 0，表示时间

    TELL(KB, MAKE-PERCEPT-SENTENCE(percept, t))
    action ← ASK(KB, MAKE-ACTION-QUERY(t))
    TELL(KB, MAKE-ACTION-SENTENCE(action, t))
    t ← t + 1
    return action

三个关键点：

• MAKE-PERCEPT-SENTENCE：把感知编码为逻辑句子（含时间戳）。
• MAKE-ACTION-QUERY：问"我在时刻 t 该做什么"。
• MAKE-ACTION-SENTENCE：必须把"我做了什么"也告诉 KB，否则智能体无法推理动作后果。

两种设计层次：

• 声明式方法（declarative）：从空 KB 开始，逐条 TELL 事实，智能体自行推理。
• 过程式方法（procedural）：直接把行为编码进程序。
  现代实用系统往往两者混合；此外还可通过学习自动向 KB 添加句子（这是与后续机器学习章节的接口）。

2.2 Wumpus World（怪兽世界）

一个 4×4 网格洞穴，PEAS 描述：

• 性能度量：拿到金子出洞 +1000；掉进坑或被 Wumpus 吃掉 −1000；每步 −1；用箭 −10。
• 环境：格子邻接。起点 [1,1] 朝右。金子、Wumpus、坑随机分布（[1,1] 除外，每格 0.2 概率是坑）。
• 执行器：Forward、TurnLeft、TurnRight、Grab、Shoot、Climb。
• 传感器（5 位向量）：
  • Stench（臭味）：与 Wumpus 相邻（非对角）
  • Breeze（微风）：与坑相邻
  • Glitter（闪光）：本格有金子
  • Bump（撞墙）：前进撞墙
  • Scream（尖叫）：Wumpus 被射死

环境属性：部分可观测、确定性、序贯、静态、离散、单智能体。

Wumpus World 的教学价值在于：局部感知 + 逻辑推理 = 全局结论。例如在 [2,1] 感到 Breeze，在 [1,2] 感到 Stench 但无 Breeze，可以严格推出 [1,3] 或 [2,2] 无坑、Wumpus 在 [1,3]、[2,2] 安全 —— 这不是猜测，是蕴涵。

2.3 逻辑的通用概念

• 语法（syntax）：规定什么样的符号串是合法句子。x + y = 4 合法，x4y+ = 不合法。
• 语义（semantics）：规定句子在每个可能世界（possible world）中的真值。可能世界的形式化即模型（model）。
• 模型（model）：对所有相关变量的一次完整赋值，是数学化的"可能世界"。若句子 $\alpha$ 在模型 $m$ 中为真，说 $m$ 满足 $\alpha$，记 $m\in M(\alpha )$，$M(\alpha )$ 为 $\alpha$ 的所有模型集合。
• 逻辑蕴涵（entailment）：

$$\alpha \models \beta ⟺M(\alpha )\subseteq M(\beta )$$

读作"$\alpha$ 蕴涵 $\beta$"，即"$\alpha$ 为真的每个模型里 $\beta$ 都为真"。注意方向：$\alpha$ 越强（模型越少），蕴涵的东西越多。

• 模型检验（model checking）：枚举所有模型，检查 $\alpha$ 为真处 $\beta$ 是否也为真。这是蕴涵的直接语义实现。
• 推导（derivation / 记作 $KB{⊢}_i\alpha$）：推理算法 $i$ 能从 KB 语法性地推出 $\alpha$。
• 可靠性（soundness / truth-preserving）：$KB{⊢}_i\alpha \Rightarrow KB\models \alpha$。只推出真的。
• 完备性（completeness）：$KB\models \alpha \Rightarrow KB{⊢}_i\alpha$。所有真的都能推出。
• 有根据性 / 落地（grounding）：逻辑符号与真实世界之间的对应关系。逻辑本身不保证 KB 里的公理为真——那来自感知与学习。这是逻辑系统与现实之间唯一无法用逻辑保证的一环。

2.4 命题逻辑（Propositional Logic）语法

BNF 文法：

Sentence        → AtomicSentence | ComplexSentence
AtomicSentence  → True | False | P | Q | R | ...
ComplexSentence → ( Sentence )
                | ¬ Sentence
                | Sentence ∧ Sentence
                | Sentence ∨ Sentence
                | Sentence ⇒ Sentence
                | Sentence ⇔ Sentence

算符优先级（从高到低）：$\neg ,\wedge ,\vee ,\Rightarrow ,\iff$

术语：

• 命题符号（proposition symbol）：$P_{1,2}$（[1,2] 有坑）、$W_{1,3}$、$B_{2,1}$ 等。
• 文字（literal）：原子句子（正文字）或其否定（负文字）。
• 子句（clause）：文字的析取，如 $\neg P\vee Q\vee \neg R$。
• 合取范式 CNF：子句的合取。
• 定子句 / Horn 子句：见 §3.4。

2.5 命题逻辑语义

模型即"每个命题符号 → {true, false}"的赋值。$n$ 个符号 ⇒ $2^n$ 个模型。

真值表递归定义：

$P$	$Q$	$\neg P$	$P\wedge Q$	$P\vee Q$	$P\Rightarrow Q$	$P\iff Q$
F	F	T	F	F	T	T
F	T	T	F	T	T	F
T	F	F	F	T	F	F
T	T	F	T	T	T	T

⚠️ 易错点：$P\Rightarrow Q$ 是实质蕴涵（material implication），$P$ 为假时整句为真。它不要求 $P$ 与 $Q$ 有任何因果或相关关系。"5 是偶数 ⇒ 上海是首都"在命题逻辑中为真。初学者必须接受这一点：$P\Rightarrow Q\equiv \neg P\vee Q$。

2.6 三个可判定性概念

概念	定义	关系
有效（valid / 重言式 tautology）	在所有模型中为真	$\alpha \models \beta ⟺(\alpha \Rightarrow \beta )$ 有效 —— 演绎定理
可满足（satisfiable）	在某个模型中为真	SAT 问题，NP-完全
不可满足（unsatisfiable）	在任何模型中都不为真	$\alpha \models \beta ⟺(\alpha \wedge \neg \beta )$ 不可满足 —— 归谬法 / refutation

最后一条是归结反演的理论基础，务必牢记。

---

3. 核心理论与算法

3.1 模型检验：TT-ENTAILS?

最朴素的完备算法：枚举所有模型。

function TT-ENTAILS?(KB, α) returns true or false
    symbols ← KB 与 α 中出现的命题符号列表
    return TT-CHECK-ALL(KB, α, symbols, {})

function TT-CHECK-ALL(KB, α, symbols, model) returns true or false
    if EMPTY?(symbols) then
        if PL-TRUE?(KB, model) then return PL-TRUE?(α, model)
        else return true              // KB 为假时该模型无约束力（空真）
    else
        P    ← FIRST(symbols)
        rest ← REST(symbols)
        return (TT-CHECK-ALL(KB, α, rest, model ∪ {P = true})
            and TT-CHECK-ALL(KB, α, rest, model ∪ {P = false}))

• 可靠且完备（对命题逻辑而言）：直接实现蕴涵定义。
• 复杂度：时间 $O(2^n)$，空间 $O(n)$（深度优先，只存一条路径）。
• 局限：$n$ 稍大即不可行；且命题逻辑的蕴涵判定本身是 co-NP-完全问题，因此不存在已知的多项式算法（除非 P = NP）。

3.2 定理证明与推理规则

不枚举模型，而在句子上做语法操作。

标准逻辑等价式（可双向替换）：

$$\begin{array}{rlrl}(\alpha \wedge \beta )& \equiv (\beta \wedge \alpha )& & \text{交换律}\\ ((\alpha \wedge \beta )\wedge \gamma )& \equiv (\alpha \wedge (\beta \wedge \gamma ))& & \text{结合律}\\ \neg (\neg \alpha )& \equiv \alpha & & \text{双重否定}\\ (\alpha \Rightarrow \beta )& \equiv (\neg \beta \Rightarrow \neg \alpha )& & \text{逆否命题 contraposition}\\ (\alpha \Rightarrow \beta )& \equiv (\neg \alpha \vee \beta )& & \text{蕴涵消去}\\ (\alpha \iff \beta )& \equiv ((\alpha \Rightarrow \beta )\wedge (\beta \Rightarrow \alpha ))& & \text{双条件消去}\\ \neg (\alpha \wedge \beta )& \equiv (\neg \alpha \vee \neg \beta )& & \text{De Morgan}\\ \neg (\alpha \vee \beta )& \equiv (\neg \alpha \wedge \neg \beta )& & \text{De Morgan}\\ (\alpha \wedge (\beta \vee \gamma ))& \equiv ((\alpha \wedge \beta )\vee (\alpha \wedge \gamma ))& & \text{分配律}\\ (\alpha \vee (\beta \wedge \gamma ))& \equiv ((\alpha \vee \beta )\wedge (\alpha \vee \gamma ))& & \text{分配律（转 CNF 的关键）}\end{array}$$

推理规则（单向产生新句子）：

• Modus Ponens（肯定前件）：$\frac{\alpha \Rightarrow \beta ,\alpha }{\beta }$
• And-Elimination（合取消去）：$\frac{\alpha \wedge \beta }{\alpha }$

把定理证明看作搜索：初始状态 = KB，动作 = 应用推理规则，目标 = 含目标句子的 KB。这就把逻辑推理和第 3 章的搜索统一起来。

重要观察：定理证明常常比模型检验高效得多，因为证明可以忽略无关命题。如果 KB 有 100 万个符号但目标只依赖其中 5 个，模型检验仍要面对 $2^{10^6}$ 的空间，而证明只需触及相关的几条句子。这就是单调性（monotonicity）带来的红利：$KB\models \alpha \Rightarrow (KB\wedge \beta )\models \alpha$，即添加新知识永远不会使已有结论失效（经典逻辑特性；非单调逻辑另论）。

3.3 归结（Resolution）—— 本章核心算法

3.3.1 归结规则

单元归结（unit resolution）：

$$\frac{{\ell }_1\vee \cdots \vee {\ell }_k,m}{{\ell }_1\vee \cdots \vee {\ell }_{i-1}\vee {\ell }_{i+1}\vee \cdots \vee {\ell }_k}({\ell }_i\text{ 与 }m\text{ 互补})$$

全归结（full resolution）：

$$\frac{{\ell }_1\vee \cdots \vee {\ell }_k,m_1\vee \cdots \vee m_n}{{\ell }_1\vee \cdots {\ell }_{i-1}\vee {\ell }_{i+1}\cdots \vee {\ell }_k\vee m_1\cdots m_{j-1}\vee m_{j+1}\cdots \vee m_n}$$

其中 ${\ell }_i$ 与 $m_j$ 是互补文字（complementary literals，一正一负的同一符号）。

结果称为归结式（resolvent）。必须对结果做因子化（factoring）：去除重复文字，例如 $(A\vee B)$ 与 $(A\vee \neg B)$ 归结得 $(A\vee A)$，须化简为 $A$。

直觉解释：${\ell }_1\vee {\ell }_2$ 与 $\neg {\ell }_2\vee {\ell }_3$ 意味着：若 ${\ell }_2$ 假则 ${\ell }_1$ 真；若 ${\ell }_2$ 真则 ${\ell }_3$ 真。无论如何 ${\ell }_1\vee {\ell }_3$ 成立。归结是"分情况讨论"的语法化。

3.3.2 转换为 CNF

归结只作用于 CNF。任何命题逻辑句子都能等价转为 CNF，步骤：

1. 消去 $\iff$：$\alpha \iff \beta \to (\alpha \Rightarrow \beta )\wedge (\beta \Rightarrow \alpha )$
2. 消去 $\Rightarrow$：$\alpha \Rightarrow \beta \to \neg \alpha \vee \beta$
3. 否定内移（De Morgan + 双重否定消去），直到 $\neg$ 只作用于原子。
4. 分配 $\vee$ 到 $\wedge$ 上：$\alpha \vee (\beta \wedge \gamma )\to (\alpha \vee \beta )\wedge (\alpha \vee \gamma )$

示例：$B_{1,1}\iff (P_{1,2}\vee P_{2,1})$

$$\begin{array}{rl}& \to (B_{1,1}\Rightarrow (P_{1,2}\vee P_{2,1}))\wedge ((P_{1,2}\vee P_{2,1})\Rightarrow B_{1,1})\\ & \to (\neg B_{1,1}\vee P_{1,2}\vee P_{2,1})\wedge (\neg (P_{1,2}\vee P_{2,1})\vee B_{1,1})\\ & \to (\neg B_{1,1}\vee P_{1,2}\vee P_{2,1})\wedge ((\neg P_{1,2}\wedge \neg P_{2,1})\vee B_{1,1})\\ & \to (\neg B_{1,1}\vee P_{1,2}\vee P_{2,1})\wedge (\neg P_{1,2}\vee B_{1,1})\wedge (\neg P_{2,1}\vee B_{1,1})\end{array}$$

⚠️ CNF 转换在最坏情况下会产生指数级膨胀。实用系统用 Tseitin 变换引入新变量，得到 SAT-等价（非逻辑等价）但规模线性的 CNF。

3.3.3 归结算法

function PL-RESOLUTION(KB, α) returns true or false
    // 判断 KB ⊨ α
    clauses ← KB ∧ ¬α 的 CNF 表示中的子句集合
    new ← {}
    loop do
        for each pair of clauses Ci, Cj in clauses do
            resolvents ← PL-RESOLVE(Ci, Cj)
            if resolvents contains the empty clause then return true
            new ← new ∪ resolvents
        if new ⊆ clauses then return false
        clauses ← clauses ∪ new

要点：

• 采用归谬法：证明 $KB\wedge \neg \alpha$ 不可满足。
• 空子句 $\square$ 代表 False（空析取为假），推出空子句即矛盾，故 $KB\models \alpha$。
• 若 new 不再产生新子句（达到不动点）而无空子句，则 $KB/\models \alpha$。

归结的完备性（Ground Resolution Theorem）：

若一个命题子句集不可满足，则对其应用归结的闭包（resolution closure）必然包含空子句。

证明思路（反证）：设闭包 $RC(S)$ 不含空子句，则可按顺序为每个符号构造一个满足赋值 $\to$ $S$ 可满足，矛盾。因此归结是反演完备的（refutation-complete）。

⚠️ 注意区分：归结不是生成完备的（不能推出所有蕴涵句子，如从 $A$ 推不出 $A\vee B$ 的直接形式），但作为反演手段是完备的——这已足够回答任何蕴涵查询。

复杂度与局限：

• 最坏情况指数时间（问题本身 co-NP-完全）。
• 子句数量爆炸是主要瓶颈，需配合策略：单元优先（unit preference）、支持集（set of support）、输入归结（input resolution）、subsumption（子句包含删除）。
• 实践中对大规模问题，DPLL/CDCL 通常优于朴素归结。

3.4 Horn 子句与定子句：前向 / 后向链接

许多真实 KB 的句子有受限形式，可用多项式算法。

• 定子句（definite clause）：恰好含一个正文字的析取子句。如 $\neg L\vee \neg B\vee A$，等价于 $(L\wedge B)\Rightarrow A$。
• Horn 子句：至多一个正文字的子句。定子句 ⊂ Horn 子句。
• 目标子句（goal clause）：无正文字的 Horn 子句。

Horn 形式的三大好处：

1. 可写成 $\text{body}\Rightarrow \text{head}$ 的蕴涵形式，接近人类直觉与规则系统。
2. 前向/后向链接推理是线性时间（关于 KB 大小）。
3. 推理步骤对人类可解释（proof tree）。

3.4.1 前向链接（Forward Chaining）—— 数据驱动

function PL-FC-ENTAILS?(KB, q) returns true or false
    // KB 为定子句集合，q 为命题符号
    count  ← 表，count[c] 初值为子句 c 的前提数目
    inferred ← 表，所有符号初值为 false
    agenda ← 队列，初值为 KB 中所有已知为真的符号（事实）

    while agenda 非空 do
        p ← POP(agenda)
        if p = q then return true
        if inferred[p] = false then
            inferred[p] ← true
            for each clause c in KB where p ∈ c.PREMISE do
                decrement count[c]
                if count[c] = 0 then add c.CONCLUSION to agenda
    return false

• 原理：从已知事实出发，反复触发前提全部满足的规则，把结论加入已知集，直到目标出现或无新结论（不动点）。
• 复杂度：$O(n)$，$n$ 为 KB 中子句体的总长度（每条子句最多触发一次，每个符号最多处理一次）。
• 可靠性：Modus Ponens 是可靠规则。
• 完备性：对定子句 KB 完备。证明思路：算法终止时把 inferred 视为模型 $m$，可证 $m$ 满足 KB 原始所有子句；因此任何 KB 蕴涵的原子必在 inferred 中。
• 适用场景：事实增量到达、需要"推出所有能推的"（如生产系统 production system、Rete 算法、数据库触发器、实时监控）。
• 局限：可能做大量与目标无关的推理（无目标导向）；不支持否定、析取结论；仅限定子句。

3.4.2 后向链接（Backward Chaining）—— 目标驱动

原理：从查询 $q$ 出发；若 $q$ 已在 KB 中为真，完成；否则找出所有结论为 $q$ 的规则，递归证明其所有前提。

function PL-BC-ENTAILS?(KB, q, visited) returns true or false
    if q 是 KB 中的已知事实 then return true
    if q ∈ visited then return false        // 防止循环
    visited ← visited ∪ {q}
    for each clause (p1 ∧ ... ∧ pk ⇒ q) in KB do
        if for all i: PL-BC-ENTAILS?(KB, pi, visited) then return true
    return false

• 搜索方式：与/或图（AND-OR graph）的深度优先搜索。规则的多个前提是 AND 分支，多条规则是 OR 分支。
• 复杂度：常常远小于线性，因为只触及与目标相关的知识子集。
• 适用场景：明确目标的查询、Prolog 与逻辑编程、专家系统的诊断问答。
• 局限：可能重复子目标（需 memoization / tabling）；左递归规则会无限循环；同样仅限定子句。

对比记忆：前向链接 = “我知道这些，能推出什么？”；后向链接 = “要证这个，需要什么？”

3.5 DPLL：高效完备的 SAT 求解

Davis–Putnam–Logemann–Loveland 算法，是现代 SAT 求解器的骨架。本质是带三大优化的回溯搜索。

function DPLL-SATISFIABLE?(s) returns true or false
    clauses ← s 的 CNF 子句集
    symbols ← s 中的命题符号列表
    return DPLL(clauses, symbols, {})

function DPLL(clauses, symbols, model) returns true or false
    if every clause in clauses is true in model  then return true
    if some clause in clauses is false in model then return false

    P, value ← FIND-PURE-SYMBOL(symbols, clauses, model)
    if P is non-null then
        return DPLL(clauses, symbols − P, model ∪ {P = value})

    P, value ← FIND-UNIT-CLAUSE(clauses, model)
    if P is non-null then
        return DPLL(clauses, symbols − P, model ∪ {P = value})

    P ← FIRST(symbols);  rest ← REST(symbols)
    return DPLL(clauses, rest, model ∪ {P = true})
        or DPLL(clauses, rest, model ∪ {P = false})

三大改进（相对朴素真值表枚举）：

1. 提前终止（early termination）：一个子句只要有一个文字为真即为真，整个 CNF 只要有一个子句为假即为假 —— 不必赋值完所有符号。
2. 纯符号启发式（pure symbol）：某符号在所有尚未满足的子句中只以同一极性出现，则可直接赋成使其为真的值，不损失可满足性。
3. 单元子句启发式（unit clause）：只剩一个未赋值文字的子句，该文字必须为真。级联应用称为单元传播（unit propagation / BCP），效果类似 CSP 中的弧相容/forward checking。

现代 SAT 求解器（CDCL）在此基础上还有：

• 成分分析（component analysis）：把独立的子问题拆开求解。
• 变量与取值次序（如 VSIDS 活跃度启发式）。
• 智能回溯（backjumping / conflict-driven clause learning）：从冲突中学习新子句（clause learning）并跳跃回溯。
• 随机重启（random restarts）与索引（watched literals，两文字观察）。

这些技术使得现代求解器能处理上千万变量的工业实例。

3.6 局部搜索：WalkSAT

不完备但对可满足实例极快。

function WALKSAT(clauses, p, max_flips) returns a model or failure
    model ← 对 clauses 中符号的随机赋值
    for i = 1 to max_flips do
        if model 满足 clauses then return model
        clause ← 随机选一个在 model 下为假的子句
        with probability p:
            翻转 clause 中随机一个符号             // 随机游走，逃出局部最优
        else:
            翻转 clause 中使满足子句数最大化的符号   // 爬山
    return failure

• 局限：不完备。返回 failure 无法区分"不可满足"与"没找够时间"。因此适合"证明可满足"，不适合"证明不可满足"。
• 应用：大规模随机实例、快速找可行解。

相变现象（phase transition）：随机 3-SAT 问题在子句/符号比 $m/n\approx 4.27$ 附近从"几乎必然可满足"急转为"几乎必然不可满足"，且该临界点附近的实例最难求解。这是理解 NP-难问题实际难度分布的重要经验规律。

3.7 命题逻辑智能体：Wumpus World 实战

3.7.1 知识库构造

对每个格子 $[x,y]$：

$$\begin{array}{rlrl}& \neg P_{1,1},\neg W_{1,1}& & \text{起点安全}\\ & B_{x,y}\iff (P_{x,y+1}\vee P_{x,y-1}\vee P_{x+1,y}\vee P_{x-1,y})& & \text{微风 ⟺ 邻格有坑}\\ & S_{x,y}\iff (W_{x,y+1}\vee W_{x,y-1}\vee W_{x+1,y}\vee W_{x-1,y})& & \text{臭味 ⟺ 邻格有 Wumpus}\\ & W_{1,1}\vee W_{1,2}\vee \cdots \vee W_{4,4}& & \text{至少一只 Wumpus}\\ & \neg W_{i,j}\vee \neg W_{k,l}\forall (i,j)\ne (k,l)& & \text{至多一只（}O(n^2)\text{ 条！）}\end{array}$$

⚠️ 注意"至多一只 Wumpus"需要 $\left(\genfrac{}{}{0ex}{}{16}{2}\right)=120$ 条子句 —— 这正是命题逻辑冗长性的直观体现。

3.7.2 时间与后继状态公理

要处理动作与时间，须给每个可变命题加时间下标：$L_{1,1}^t$（时刻 t 在 [1,1]）、$FacingRigh{t}^t$、$HaveArro{w}^t$。

• 流（fluent）：随时间改变的命题，如位置、朝向。
• 非流 / 永久符号（atemporal symbols）：$P_{1,2}$、$W_{1,3}$ 等不随时间变化。

转移模型用后继状态公理（successor-state axiom）表达：

$$F^{t+1}\iff {\text{ActionCausesF}}^t\vee (F^t\wedge \neg {\text{ActionCausesNotF}}^t)$$

例如：

$$HaveArro{w}^{t+1}\iff (HaveArro{w}^t\wedge \neg Shoo{t}^t)$$

$$\begin{array}{rl}{L}_{1,1}^{t+1}\iff & (L_{1,1}^t\wedge (\neg Forwar{d}^t\vee Bum{p}^{t+1}))\\ \vee & (L_{1,2}^t\wedge (FacingDow{n}^t\wedge Forwar{d}^t))\\ \vee & (L_{2,1}^t\wedge (FacingLef{t}^t\wedge Forwar{d}^t))\end{array}$$

框架问题（frame problem）：如何简洁表达"动作没有改变的一切"？

• 朴素做法需要 $O(|A|\times |F|)$ 条框架公理（frame axiom），荒谬地冗长。
• 后继状态公理（Reiter）以 $O(|F|)$ 条解决表示性框架问题（representational frame problem）。
• 推理性框架问题（inferential frame problem）：即使表示简洁，推理时仍需逐时间步传播所有不变流 —— 需要状态估计等技术缓解。

状态估计（state estimation）：与其保存整个历史 KB，不如维护一个信念状态（belief state）——对当前可能世界集合的逻辑描述。精确信念状态可能指数大，实用做法是维护一个保守近似（如只保留字面量的合取，即 1-CNF 信念状态），牺牲部分推理能力换取线性更新代价。这是第 4/11/12 章"信念状态"思想在逻辑框架下的体现。

3.7.3 混合智能体（Hybrid Agent）

把逻辑推理与问题求解搜索结合：

function HYBRID-WUMPUS-AGENT(percept) returns an action
    persistent: KB; t ← 0; plan ← []

    TELL(KB, 时刻 t 的感知语句)
    TELL(KB, 时刻 t 的永久/后继状态公理)
    safe ← { [x,y] : ASK(KB, OK^t_{x,y}) = true }

    if ASK(KB, Glitter^t) = true then
        plan ← [Grab] + PLAN-ROUTE(current, {[1,1]}, safe) + [Climb]

    if plan 为空 then
        unvisited ← { [x,y] : ASK(KB, L^{t'}_{x,y}) = false, ∀ t' ≤ t }
        plan ← PLAN-ROUTE(current, unvisited ∩ safe, safe)

    if plan 为空 and ASK(KB, HaveArrow^t) = true then
        possible_wumpus ← { [x,y] : ASK(KB, ¬W_{x,y}) = false }
        plan ← PLAN-SHOT(current, possible_wumpus, safe)

    if plan 为空 then                       // 冒险：走"未被证明不安全"的格子
        not_unsafe ← { [x,y] : ASK(KB, ¬OK^t_{x,y}) = false }
        plan ← PLAN-ROUTE(current, unvisited ∩ not_unsafe, safe)

    if plan 为空 then
        plan ← PLAN-ROUTE(current, {[1,1]}, safe) + [Climb]

    action ← POP(plan)
    TELL(KB, MAKE-ACTION-SENTENCE(action, t));  t ← t + 1
    return action

注意其优先级排序体现了"安全 > 收益 > 探索 > 冒险 > 撤退"的策略，PLAN-ROUTE 用第 3 章的 A* 在安全格子图上寻路。

3.8 SATPlan：把规划编译成 SAT

思路：规划 = 找一个使"初始状态 ∧ 转移 ∧ 目标"可满足的模型。

function SATPLAN(init, transition, goal, T_max) returns solution or failure
    for t = 0 to T_max do
        cnf, mapping ← TRANSLATE-TO-SAT(init, transition, goal, t)
        model ← SAT-SOLVER(cnf)
        if model is not null then
            return EXTRACT-SOLUTION(model, mapping)
    return failure

构造要点：

1. 把初始状态、每步的后继状态公理、时刻 $t$ 的目标断言全部合取成一个大 CNF。
2. 逐步加长时间视界 $t=0,1,2,\dots$（迭代加深），保证找到最短方案。
3. 必须加前提公理（precondition axiom）：动作发生则前提成立。
4. 必须加动作互斥公理（action exclusion axiom）：同一时刻至多一个动作，否则求解器会返回"同时前进又转身"的伪方案。

优点：

• 直接享受 SAT 求解器数十年的工程红利（CDCL、启发式）。
• 表达灵活，容易加入领域约束。

局限：

• 需要上界 $T_{max}$，实质是有界模型检验（bounded model checking），无法证明"不可解"。
• 命题化导致公式规模随对象数、时间步多项式甚至指数增长（grounding blow-up）。
• 优化目标（代价最小）难以自然表达，需 MaxSAT / PB 约束扩展。

这条路线在第 11 章还会以 Graphplan / 基于 SAT 的规划的形式重现。

3.8.1 SATPLAN 算法详细实现

以下是 SATPLAN 算法的完整伪代码实现，包含迭代加深、CNF构造和动作互斥约束等关键步骤：

function SATPLAN(init, transition, goal, T_max) returns solution or failure
    # 输入：
    #   init: 初始状态命题集合（如 L₀¹,₁, HaveArrow₀, ...）
    #   transition: 转移模型（后继状态公理、前提公理等）
    #   goal: 目标状态命题（如 HaveGoldₜ ∧ Lₜ¹,₁）
    #   T_max: 最大时间步上界
    # 输出：动作序列 [a₀, a₁, ..., aₜ₋₁] 或 failure
    
    for t = 0 to T_max do
        # 步骤1：构造时间步 t 的命题化 CNF
        cnf, mapping ← TRANSLATE-TO-SAT(init, transition, goal, t)
        
        # 步骤2：调用 SAT 求解器
        model ← SAT-SOLVER(cnf)  # 使用 DPLL/CDCL 等
        
        if model is not null then
            # 步骤3：从模型中提取动作序列
            return EXTRACT-SOLUTION(model, mapping)
    
    return failure  # 在 T_max 内未找到解

function TRANSLATE-TO-SAT(init, transition, goal, t) returns (cnf, mapping)
    # 初始化 CNF 子句集合
    cnf ← []
    mapping ← {}  # 记录命题符号到变量的映射
    
    # 1. 初始状态约束（时刻 0）
    for each fluent f in init do
        var ← CREATE-VARIABLE(f, 0)  # 创建命题变量，如 L₀¹,₁
        cnf.append([var])            # 单文字子句，表示 f 在时刻 0 为真
        mapping[f,0] ← var
    
    # 2. 目标状态约束（时刻 t）
    for each fluent f in goal do
        var ← CREATE-VARIABLE(f, t)
        cnf.append([var])            # 目标必须在时刻 t 成立
        mapping[f,t] ← var
    
    # 3. 后继状态公理（对所有流和所有时间步 0 ≤ τ < t）
    for τ = 0 to t-1 do
        for each fluent f do
            # 后继状态公理：F^{τ+1} ⇔ ActionCausesFᵗ ∨ (Fᵗ ∧ ¬ActionCausesNotFᵗ)
            # 转换为 CNF 形式
            f_next ← CREATE-VARIABLE(f, τ+1)
            f_curr ← CREATE-VARIABLE(f, τ)
            
            # 获取使 f 为真的动作集合（因果律）
            causes_f ← GET-ACTION-CAUSES(f, τ)
            # 获取使 f 为假的动作集合
            causes_not_f ← GET-ACTION-CAUSES-NOT(f, τ)
            
            # 构造 CNF 子句
            # (1) f_next ∨ ¬(任何使 f 为真的动作) ∨ ¬f_curr
            # (2) ¬f_next ∨ (某个使 f 为真的动作) ∨ f_curr
            # (3) f_next ∨ (某个使 f 为假的动作) ∨ ¬f_curr
            # (4) ¬f_next ∨ ¬(任何使 f 为假的动作) ∨ f_curr
            # 具体实现需根据领域动作细化
            
            cnf.extend(ENCODE-SUCCESSOR-AXIOM(f_curr, f_next, causes_f, causes_not_f, τ))
    
    # 4. 前提公理（动作发生则其前提必须满足）
    for τ = 0 to t-1 do
        for each action a do
            a_var ← CREATE-VARIABLE(a, τ)  # 动作变量，如 Forwardₜ
            preconditions ← GET-PRECONDITIONS(a, τ)
            # 编码：a_var ⇒ ∧preconditions
            # 转换为 CNF：¬a_var ∨ pre₁, ¬a_var ∨ pre₂, ...
            for each pre in preconditions do
                pre_var ← CREATE-VARIABLE(pre, τ)
                cnf.append([-a_var, pre_var])  # ¬a ∨ pre
    
    # 5. 动作互斥公理（同一时刻至多一个动作）
    for τ = 0 to t-1 do
        actions ← GET-ALL-ACTIONS()
        # 对每对不同的动作 (aᵢ, aⱼ)，添加 ¬aᵢ ∨ ¬aⱼ
        for i = 0 to |actions|-1 do
            for j = i+1 to |actions|-1 do
                a_i_var ← CREATE-VARIABLE(actions[i], τ)
                a_j_var ← CREATE-VARIABLE(actions[j], τ)
                cnf.append([-a_i_var, -a_j_var])  # 互斥约束
    
    # 6. 框架公理简化版（可选，后继状态公理已隐含）
    # 传统框架公理：¬ActionAffectsFᵗ ⇒ (Fᵗ⁺¹ ⇔ Fᵗ)
    # 但后继状态公理已更紧凑地编码了变化
    
    return cnf, mapping

function EXTRACT-SOLUTION(model, mapping) returns action_sequence
    # 从满足的模型中提取动作序列
    action_sequence ← []
    
    # 找出所有为真的动作变量，按时间排序
    for each (symbol, time) in mapping.keys do
        if symbol is an action and model[mapping[symbol,time]] = true then
            action_sequence[time] ← symbol
    
    # 确保动作序列连续（无时间间隙）
    return action_sequence

3.8.2 关键步骤注释

1. 迭代加深（Iterative Deepening）：

   • 外层循环 for t = 0 to T_max 逐步增加时间步上限
   • 保证找到最短规划（若有解）
   • 本质是有界模型检验（Bounded Model Checking）

2. CNF 构造细节：

   • 初始状态：每个在时刻0为真的流表示为单文字子句
   • 目标状态：每个在时刻t为真的流表示为单文字子句
   • 后继状态公理：对每个流f和每个时间步τ，编码 F^{τ+1} ⇔ ActionCausesFᵗ ∨ (Fᵗ ∧ ¬ActionCausesNotFᵗ)
   • 前提公理：Actionᵗ ⇒ Precondition₁ᵗ ∧ ... ∧ Preconditionₖᵗ
   • 动作互斥：对每对不同的动作aᵢ, aⱼ，¬aᵢᵗ ∨ ¬aⱼᵗ（同一时刻只能执行一个动作）

3. 动作互斥约束的必要性：

   • 防止求解器返回"同时前进又左转"的无效规划
   • 在经典规划中通常假设动作是原子的（atomic）
   • 对于并发动作，需替换为更精细的互斥关系（如 Graphplan 的互斥动作对）

4. 命题化（Grounding）的规模：

   • 变量数 ≈ |F| × (t+1) + |A| × t，其中|F|是流数量，|A|是动作数量
   • 子句数 ≈ O(t × (|F| + |A|²))，最坏情况随t和|A|²增长

3.8.3 复杂度分析

时间复杂度：

1. 命题化阶段：O(t × (|F| + |A|²))，多项式时间
2. SAT求解阶段：最坏情况指数时间（SAT是NP完全问题）
   • 实际性能依赖现代SAT求解器（CDCL）的启发式
   • 对于规划问题，结构通常比随机SAT更简单

空间复杂度：

• 变量数：O(t × (|F| + |A|))
• 子句数：O(t × (|F| + |A|²))
• 实际编码中可通过避免完全实例化优化：
  • 使用** lifted 编码**（一阶逻辑层面编码，再命题化）
  • 对称性打破（symmetry breaking）减少搜索空间

与搜索算法的对比：

• 优势：直接利用高效SAT求解器，避免自定义搜索启发式
• 劣势：需要预先指定时间上界T_max，无法证明无解（除非T_max足够大）
• 适用场景：中等规模确定性规划、形式验证、调度问题

扩展变体：

1. 并行SATPlan：同时求解多个t值，利用多核
2. 增量SAT：重用t-1步的求解结果加速t步求解
3. 最优SATPlan：添加代价约束，使用MaxSAT或PB（Pseudo-Boolean）求解器
4. 部分有序SATPlan：放松动作完全有序约束，使用SMT求解器

实例：Wumpus World中的SATPlan

• 流：Lˣ,ʸᵗ（位置）、FacingRightᵗ、HaveArrowᵗ、HaveGoldᵗ、WumpusAliveᵗ
• 动作：Forwardᵗ、TurnLeftᵗ、TurnRightᵗ、Grabᵗ、Shootᵗ、Climbᵗ
• 对于4×4网格，|F| ≈ 30，|A| = 6
• 规划长度t=10时，变量数 ≈ 30×11 + 6×10 = 390，在现代SAT求解器能力范围内

SATPlan展示了逻辑作为通用求解基底的威力：将规划问题归约到SAT，直接享受SAT求解器数十年的优化成果。这种"编译"思路在第11章（规划）和第9章（一阶逻辑推理）中进一步深化。

3.9 命题逻辑的根本局限

1. 缺乏表达力：不能说"所有相邻有坑的格子都有微风"，只能对每个格子写一条，共 $O(n)$ 甚至 $O(n^2)$ 条。
2. 对象与关系不可见：$P_{1,2}$ 只是一个不透明符号，逻辑系统看不到"[1,2] 是一个位置"、“Pit 是一种事物”。
3. 无法处理未知数量的对象：命题符号集合必须预先固定。
4. 无变量、无量化：无法陈述通用规律，知识不可迁移。

⇒ 需要一阶逻辑（First-Order Logic）：引入对象（object）、关系（relation）、函数（function）、量词（$\forall ,\exists$），把 $O(n^2)$ 条命题句压缩成一条普适规则。这正是第 8 章的主题。

---

4. 关键图示/表格说明

4.1 蕴涵的语义图（对应原书 Figure 7.6）

想象两个椭圆区域：

所有可能世界（模型）
┌──────────────────────────────────────┐
│                                      │
│    ┌──────────────────────────┐      │
│    │   M(β)  —— β 为真的模型   │      │
│    │                          │      │
│    │   ┌──────────────┐       │      │
│    │   │  M(KB)       │       │      │
│    │   │ KB 为真的模型 │       │      │
│    │   └──────────────┘       │      │
│    └──────────────────────────┘      │
└──────────────────────────────────────┘
        KB ⊨ β  ⟺  M(KB) ⊆ M(β)

读图要点：KB 越强 → $M(KB)$ 越小 → 蕴涵的句子越多。极端情形：KB 不可满足（$M(KB)=\varnothing$）时蕴涵一切句子（爆炸原理 ex falso quodlibet）—— 这解释了为什么"知识库中的矛盾"是致命的。

4.2 Wumpus World 推理过程（对应原书 Figure 7.3–7.4）

步骤	位置	感知	推理结论
1	[1,1]	无 Stench、无 Breeze	[1,2]、[2,1] 均 OK（安全）
2	[2,1]	Breeze	[2,2] 或 [3,1] 有坑（至少一个）
3	回退到 [1,2]	Stench，无 Breeze	无 Breeze ⇒ [2,2] 无坑 ⇒ 结合步 2，[3,1] 有坑 Stench 且 [2,2]、[1,1] 已排除 Wumpus ⇒ W 在 [1,3]
4	[2,2]	无感知	[2,3]、[3,2] 均 OK

这张表是全章精髓：单个感知不足以定论，多个局部感知的组合通过蕴涵产生确定的全局结论。步骤 3 用到了 modus tollens 式推理（无微风 ⇒ 邻格无坑），是典型的"从否定信息中获取信息"。

智能体决策循环流程图：

该流程图展示了混合智能体（§3.7.3）的核心决策循环：从感知输入开始，更新知识库，查询安全格子，根据当前目标（取金、射杀Wumpus、探索、撤退）规划路径，执行动作并记录到KB，然后进入下一时间步。循环体现了感知→推理→行动的完整链条，以及安全优先的决策逻辑。

4.3 逻辑连接词真值表

见 §2.5。复习要点：只需记住 $P\Rightarrow Q\equiv \neg P\vee Q$ 和 De Morgan，其余可推。

4.4 三类推理算法对比表

算法	输入限制	可靠	完备	时间复杂度	典型场景
TT-ENTAILS?（真值表）	任意命题句	✓	✓	$O(2^n)$	教学、极小规模
PL-RESOLUTION	CNF	✓	✓（反演完备）	最坏指数	通用定理证明
PL-FC-ENTAILS?（前向链接）	定子句	✓	✓（定子句范围）	$O(n)$ 线性	生产系统、数据驱动监控
PL-BC-ENTAILS?（后向链接）	定子句	✓	✓（定子句范围）	常常 ≪ 线性	Prolog、目标驱动诊断
DPLL / CDCL	CNF（SAT 判定）	✓	✓	最坏指数，实践极快	工业级 SAT、硬件验证
WalkSAT	CNF	✓（找到解时）	✗	无界	大规模可满足实例

4.5 逻辑表示与其他表示的层级（对应第 2 章表示谱系）

表示层级	世界的结构	代表章节
原子（atomic）	状态不可分割	第 3 章搜索
因子化（factored）	状态 = 变量集合	第 6 章 CSP、第 7 章命题逻辑
结构化（structured）	对象 + 关系	第 8–12 章一阶逻辑

命题逻辑处在"因子化"的最上层：它比 CSP 表达力更强（支持任意布尔组合与蕴涵推理），但仍未触及对象与关系。

4.6 归结证明树示例

证明 Wumpus World 中 $\neg P_{1,2}$（[1,2] 无坑），已知 $\neg B_{1,1}$ 与 $B_{1,1}\iff (P_{1,2}\vee P_{2,1})$：

CNF 子句：
  C1: ¬B₁,₁ ∨ P₁,₂ ∨ P₂,₁
  C2: ¬P₁,₂ ∨ B₁,₁
  C3: ¬P₂,₁ ∨ B₁,₁
  C4: ¬B₁,₁              (感知)
  C5: P₁,₂               (¬α，取否定目标)

归结过程：
  C2 + C4  →  ¬P₁,₂            (消去 B₁,₁)
  上式 + C5 →  □  (空子句)      ⇒ 矛盾 ⇒ KB ⊨ ¬P₁,₂  ✓

这个 3 步证明说明：归结找到的证明往往极短，远比枚举 $2^n$ 个模型高效。

---

5. 与其他章节的关联

5.1 向前回溯

章节	关联点
第 2 章 智能体	本章的知识型智能体是"基于模型的反射型智能体 / 目标型智能体"的逻辑化实现；表示谱系（原子/因子化/结构化）在此落地
第 3–4 章 搜索	定理证明本身被建模为搜索问题；混合 Wumpus 智能体内部用 A* 做 PLAN-ROUTE；SATPlan 用迭代加深思路控制时间视界
第 5 章 博弈	对抗环境下也可用逻辑推理对手能力，但博弈更多依赖效用与搜索
第 6 章 CSP	联系最紧密：SAT 是 CSP 的布尔特例；DPLL 的单元传播 ≈ CSP 的弧相容；纯符号 ≈ 值对称性剪枝；CDCL 的冲突学习 ≈ CSP 的 conflict-directed backjumping + nogood learning

5.2 向后展开

章节	关联点
第 8 章 一阶逻辑	直接由本章 §3.9 的局限引出。FOL 用 $\forall x$ 把 $O(n^2)$ 条命题句压成一条
第 9 章 FOL 推理	归结提升为 lifted resolution（配合 unification）；前向/后向链接扩展为 Datalog 与 Prolog
第 10 章 知识表示	讨论"用什么内容填充 KB"——本体、类别、事件、时空；本章解决"怎样表示与推理"的机制
第 11 章 自动规划	SATPlan 的完整展开；PDDL 的语义可用逻辑给出；Graphplan 的互斥关系与 SAT 编码的互斥公理同源
第 12 章 机器人知识表示	后继状态公理演化为 situation calculus 与 event calculus；框架问题在此得到系统处理
第 13–17 章 概率推理	命题逻辑的"真/假"二值被概率取代；贝叶斯网络可视为"带不确定性的因子化表示"；本章的确定性推理是概率推理在 p∈{0,1}p\in\{0,1\}p∈{0,1} 时的退化情形
第 19–22 章 学习	逻辑 KB 可由学习获得（归纳逻辑编程 ILP，第 19 章）；神经网络学到的是隐式知识，与显式 KB 形成互补

5.3 概念承接主线

命题逻辑（第7章）
   │ 表达力不足（无对象/关系/量词）
   ↓
一阶逻辑（第8章）—— 语法与语义
   │ 需要高效推理机制
   ↓
FOL 推理（第9章）—— unification / lifted resolution
   │ 需要具体内容填充
   ↓
知识表示（第10章）—— 本体、类别、事件
   │ 应用到"如何行动"
   ↓
自动规划（第11章）+ 机器人 KR（第12章）

---

6. 延伸思考

6.1 大语言模型是"逻辑智能体"吗？—— 神经-符号的张力

LLM 在数学与逻辑推理基准上表现惊人，但其机制与本章的逻辑智能体截然不同：

维度	本章逻辑智能体	大语言模型
知识形式	显式句子，可读可编辑	隐式权重，难以定位与修改
推理保证	可靠 + 完备（可证明）	无保证，可能产生"看起来对"的错误链
一致性	矛盾可检测（推出 $\square$）	可能同时给出矛盾断言而不自知
单调性	满足单调性	上下文改变可致结论翻转
可解释性	有证明树	思维链（CoT）只是事后叙述，未必反映真实计算

开放性问题 1：

LLM 的思维链（chain-of-thought）与本章的证明树在形式上都是"一串推理步骤"，但前者不保证每一步可靠。是否可以构建一种混合架构：LLM 负责"猜测证明结构"（提出引理、选择推理规则），符号引擎负责"验证每一步"？这正是 AlphaGeometry、LeanDojo、DeepSeek-Prover 等系统的思路——LLM 作为启发式函数，定理证明器作为可靠性保障。

进一步追问：

• 本章讲的"归结的搜索空间爆炸"是符号方法的核心瓶颈；LLM 恰好擅长在巨大空间中做有品味的剪枝。能否把 DPLL 的变量选择启发式（VSIDS）替换为学习得到的策略？（已有 NeuroSAT、Graph Neural Network for SAT 等工作，但在工业实例上尚未全面超越手工启发式。）
• 反过来，符号引擎能否为 LLM 提供训练信号？例如用 SAT 求解器自动生成海量"带证明的推理题"，以逻辑正确性为奖励做 RL —— 这是"过程监督"（process supervision）思路的逻辑学版本。

6.2 知识库的可审计性与 AI 对齐

本章的 KB 有一个被低估的性质：可审计性（auditability）。任何结论都能追溯到具体公理 + 具体推理步骤。而 LLM 给出"不应执行此操作"时，我们无法确知它依据的是什么。

开放性问题 2：

在 AI 对齐（alignment）语境下，能否把关键的安全约束表达为显式的逻辑句子（如"不得输出可用于合成危险物质的具体步骤"），并用可靠的推理引擎在模型输出前后做形式化检查（runtime verification / shielding）？

这条路线的深层困难恰恰是本章末尾的落地问题（grounding）：

1. 符号落地难题：安全规则必须引用现实概念（“危险”、“伤害”、“欺骗”），而这些概念在开放世界中无法被完全形式化。逻辑的可靠性只保证"从公理到结论"，不保证"公理本身对应现实"。
2. 单调性与情境：经典逻辑的单调性意味着"新信息不推翻旧结论"，但真实伦理判断高度依赖情境，往往需要非单调逻辑（默认推理 default reasoning、可废止推理 defeasible reasoning）。
3. 计算不可行：完整的一致性检查对大规模 KB 是 co-NP-难的。实时系统只能做近似检查——这正是 §3.7 中"保守近似信念状态"思想的伦理版本。

一个具体可操作的思考：

与其追求"用逻辑约束整个 LLM"，不如把逻辑用在接口层：在 Agent 调用工具（执行代码、发邮件、转账）之前，用一个小型 SAT/SMT 求解器检查"本次动作 ∧ 安全公理"是否可满足。这既保留了 LLM 的开放能力，又在高风险的、可形式化的动作边界上获得了硬保证。这与 §3.7 混合智能体"安全 > 收益 > 探索"的优先级排序精神完全一致——Wumpus 智能体只走能被证明安全的格子，除非无路可走。

6.3 多模态与"感知到符号"的鸿沟

Wumpus 智能体的感知 Breeze 是被免费给定的干净符号。真实机器人拿到的是像素与点云。

• 从多模态输入到逻辑原子的映射（感知落地）本身就是一个有噪声、有歧义的推断问题。
• 一旦感知有错，命题逻辑的"爆炸原理"会使整个 KB 失效（矛盾蕴涵一切）。这正是概率推理（第 12–17 章）不可回避的原因。
• 折中路线：概率软逻辑（Markov Logic Networks、ProbLog）给每条逻辑规则一个权重，用逻辑结构描述知识、用概率吸收噪声。多模态大模型 + 概率逻辑，可能是"让机器人真正在开放世界中做可靠推理"的方向。

收束思考：本章教给我们的不只是归结与 DPLL，而是一种方法论姿态——把"知识"与"推理"分离，使系统的行为可追溯、可修改、可证明。在深度学习主导的今天，这种姿态非但没有过时，反而在"AI 可信性"成为核心议题时显得愈发关键。