Week 3: 模态逻辑语义

COMP304/521 知识表示与推理
Knowledge Representation & Reasoning

---

目录

1. 可能世界
2. 模型的形式化定义
3. 模态逻辑的语义规则
4. 模型检查方法
5. 端点的特殊性质
6. 多智能体预告
7. 练习题
8. 考试重点

---

1. 可能世界（Possible Worlds）

1.1 什么是可能世界？

定义：可能世界是对宇宙某个可能状态的描述（或至少是我们关心的那部分）。

核心思想： - 在命题逻辑中，公式的真值由一个赋值决定 - 在模态逻辑中，公式的真值由一个世界决定

例子：假设我们只关心"此刻利物浦是否下雨"

可能世界1 (w1): 正在下雨
可能世界2 (w2): 没有下雨

关键理解： - 其中一个是真实世界（actual world） - 另一个是假设的替代世界（hypothetical alternative） - 我们可能不知道哪个是真实的

1.2 真值相对于世界

命题逻辑 vs 模态逻辑：

命题逻辑：
问题："p为真吗？"
需要：一个赋值 V

模态逻辑：
问题："p为真吗？"
需要：指定在哪个世界！
答案：M, w1 ⊨ p  (在世界w1中，p为真)
M, w2 ⊭ p  (在世界w2中，p为假)

例子：\(p =\) "正在下雨"

世界w1 (下雨世界):    M, w1 ⊨ p   ✓
世界w2 (不下雨世界):  M, w2 ⊭ p   ✗

1.3 世界之间的关系

关键思想：世界之间有箭头（Arrows）连接，表示可达性关系（Accessibility Relation）。

关系的含义（取决于模态逻辑的类型）：

逻辑类型	\(w_1 \rightarrow w_2\) 的含义
Epistemic	在\(w_1\)中，我认为\(w_2\)可能是真实世界
Alethic	从\(w_1\)的角度看，\(w_2\)是一个可能的世界
Temporal	从\(w_1\)可以到达未来的\(w_2\)

1.4 无窗房间例子（Epistemic逻辑）

情境：你在无窗房间里，无法观察外面是否下雨。

模型图：

    w1 (下雨)  ←→  w2 (不下雨)
        ↻            ↻
    ```

**解释**：
- **w1 → w2**：在下雨世界，你无法确定不在不下雨世界
- **w2 → w1**：在不下雨世界，你无法确定不在下雨世界
- **自反箭头**：你总认为当前世界可能是真实的

**对比：有窗房间**

**情境**：你在有窗房间里，可以看到外面。

**模型图**：

w1 (下雨)      w2 (不下雨)
    ↻              ↻
```

解释： - 无w1 → w2：如果在下雨世界，通过窗户看到下雨，确定不在不下雨世界 - 无w2 → w1：如果在不下雨世界，看到不下雨，确定不在下雨世界 - 只有自反箭头

---

2. 模型的形式化定义

2.1 模型的三元组结构

定义：模型 \(M\) 是一个三元组 \(M = (W, R, V)\)，其中：

1. \(W\)：可能世界的集合（Set of Possible Worlds）

例子：W = {w1, w2, w3, w4}

2. \(R \subseteq W \times W\)：可达性关系（Accessibility Relation）

例子：R = {(w1, w2), (w2, w3), (w3, w4), (w4, w2)}
解释：w1能到达w2，w2能到达w3，...

3. \(V: \mathbb{P} \rightarrow 2^W\)：赋值函数（Valuation Function）

例子：V(p) = {w1, w3}
解释：p在w1和w3为真，在其他世界为假

⭐ 符号说明： - \(2^W\)：\(W\) 的幂集（所有子集的集合） - \(V(p)\)：使 \(p\) 为真的所有世界的集合

2.2 模型的图形表示

规则： 1. 每个世界画成一个圆圈 2. 世界中为真的原子命题标注在圆圈内 3. 关系 \((w_i, w_j) \in R\) 画成从 \(w_i\) 到 \(w_j\) 的箭头

例子：

模型 M = (W, R, V) 其中：

- W = {w1, w2, w3}
- R = {(w1, w2), (w2, w3), (w3, w2), (w3, w1)}
- V(p) = {w1}, V(q) = {w1, w2}

图形表示：

    w1 ----→ w2
    p,q        q
↑       ↙ ↖
└── w3 ──┘

⚠️ 注意： - 为真的命题标注在世界内（如 \(p, q\)） - 不标注 \(\neg p\)（不为真的就不标） - 箭头方向很重要！

2.3 后继（Successor）概念

定义：如果 \((w, w') \in R\)，则称 \(w'\) 是 \(w\) 的后继（Successor）。

记号： [ Succ(w) = {w' \in W \mid (w, w') \in R} ]

例子：

给定模型：
w1 → w2 → w3 → w4
↻

则：

- Succ(w1) = {w2}
- Succ(w2) = {w2, w3}  (自己+w3)
- Succ(w3) = {w4}
- Succ(w4) = ∅  (空集，没有后继)

---

3. 模态逻辑的语义规则

3.1 指定模型（Pointed Model）

定义：指定模型是一个二元组 \(M, w\)，其中： - \(M\) 是一个模型 - \(w \in W\) 是 \(M\) 中的一个世界

记号：\(M, w \models \phi\)
读作："在模型 \(M\) 的世界 \(w\) 中，\(\phi\) 为真"

同义表达： - \(\phi\) holds in \(M, w\) - \(\phi\) is satisfied in \(M, w\) - \(\phi\) is true in \(M, w\)

3.2 五大语义规则

给定模型 \(M = (W, R, V)\) 和世界 \(w \in W\)：

规则1：原子命题（Atomic Proposition）

\[ M, w \models p \iff w \in V(p) \]

含义：\(p\) 在 \(w\) 为真，当且仅当 \(w\) 在 \(p\) 的赋值集合中。

例子：

V(p) = {w1, w3}

M, w1 ⊨ p  ✓  (因为 w1 ∈ V(p))
M, w2 ⊭ p  ✗  (因为 w2 ∉ V(p))
M, w3 ⊨ p  ✓  (因为 w3 ∈ V(p))

规则2：否定（Negation）

\[ M, w \models \neg \phi \iff M, w \not\models \phi \]

含义：\(\neg \phi\) 在 \(w\) 为真，当且仅当 \(\phi\) 在 \(w\) 为假。

规则3：合取（Conjunction）

\[ M, w \models \phi \land \psi \iff M, w \models \phi \text{ 且 } M, w \models \psi \]

含义：\(\phi \land \psi\) 在 \(w\) 为真，当且仅当 \(\phi\) 和 \(\psi\) 都在 \(w\) 为真。

⚠️ 注意：这三条规则与命题逻辑完全相同！

规则4：Box（⭐ 核心规则）

\[ M, w \models \Box \phi \iff \text{对于所有 } w' \text{ 使得 } (w, w') \in R, \text{ 有 } M, w' \models \phi \]

简化表达： [ M, w \models \Box \phi \iff \text{对于所有后继 } w' \text{ of } w, \text{ 有 } M, w' \models \phi ]

含义：\(\Box \phi\) 在 \(w\) 为真，当且仅当 \(\phi\) 在 \(w\) 的所有后继中都为真。

记忆法： - Box = All successors（所有后继） - "必然"需要在所有可能世界都成立

例子：

模型：
w1 → w2 → w3
p,q    q

问题：M, w1 ⊨ □q ?

步骤：

1. 找w1的后继：Succ(w1) = {w2}
2. 检查q在所有后继中是否为真：
M, w2 ⊨ q?  → w2 ∈ V(q) → ✓
3. 结论：M, w1 ⊨ □q  ✓

规则5：Diamond（推导规则）

定义：\(\Diamond \phi \coloneqq \neg \Box \neg \phi\)

推导过程（重要！考试常考）：

步骤1：M, w ⊨ ◇φ  (定义)
⟺ M, w ⊨ ¬□¬φ

步骤2：(否定规则)
⟺ M, w ⊭ □¬φ

步骤3：(Box规则否定)
⟺ 不是所有后继 w' 满足 M, w' ⊨ ¬φ

步骤4：(逻辑等价)
⟺ 至少存在一个后继 w' 满足 M, w' ⊭ ¬φ

步骤5：(双重否定)
⟺ 至少存在一个后继 w' 满足 M, w' ⊨ φ

最终规则： [ M, w \models \Diamond \phi \iff \text{存在至少一个后继 } w' \text{ of } w \text{ 使得 } M, w' \models \phi ]

记忆法： - Diamond = At least one successor（至少一个后继） - "可能"只需要存在一个可能世界成立

3.3 有效性（Validity）

定义：公式 \(\phi\) 是有效的（Valid），记作 \(\models \phi\)，当且仅当： [ \text{对于所有模型 } M \text{ 和所有世界 } w \in M, \text{ 有 } M, w \models \phi ]

含义：\(\phi\) 在任何指定模型中都为真。

例子： - ✅ \(\models p \lor \neg p\)（排中律，命题逻辑永真式） - ✅ \(\models \Box(p \rightarrow q) \rightarrow (\Box p \rightarrow \Box q)\)（K公理） - ❌ \(\not\models \Box p\)（不是永真的，取决于模型）

---

4. 模型检查方法（Model Checking）

4.1 什么是模型检查？

问题：给定模型 \(M\)、世界 \(w\) 和公式 \(\phi\)，判断 \(M, w \models \phi\) 是否成立。

两种策略： 1. Top-down（自上而下）：从完整公式开始分解 2. Bottom-up（自下而上）：从原子命题开始构建

4.2 Top-down策略

思路：从完整公式开始，逐层分解为子公式，递归检查。

步骤： 1. 识别最外层连接词 2. 应用相应语义规则 3. 递归处理子公式 4. 构建决策树

优点： - 思路直观 - 可以提前终止（如 \(\Box \phi\) 在第一个后继就失败）

缺点： - 嵌套深时容易出错 - 可能重复计算相同子公式

例题：判断 \(M, w_1 \models \Box(p \lor \Diamond q)\)

模型 M:
w1 → w2 → w3
p,q    q

步骤1：识别最外层连接词 → □
需要检查：p ∨ ◇q 在所有后继中是否为真

步骤2：找w1的后继
Succ(w1) = {w2}

步骤3：检查 M, w2 ⊨ p ∨ ◇q

步骤3.1：检查 M, w2 ⊨ p
w2 ∉ V(p) → ✗

步骤3.2：检查 M, w2 ⊨ ◇q
需要找w2的后继：Succ(w2) = {w3}
检查 M, w3 ⊨ q → w3 ∈ V(q) → ✓
因此 M, w2 ⊨ ◇q  ✓

步骤3.3：M, w2 ⊨ p ∨ ◇q → 0 ∨ 1 = 1  ✓

步骤4：所有后继都满足 p ∨ ◇q
因此 M, w1 ⊨ □(p ∨ ◇q)  ✓

4.3 Bottom-up策略

思路：从原子命题开始，逐步计算更复杂公式的真值，直到目标公式。

步骤： 1. 列出所有原子命题在每个世界的真值 2. 计算简单公式（如 \(\neg p\)）在每个世界的真值 3. 逐步计算更复杂公式 4. 最终得到目标公式的真值

优点： - 系统化，不易出错 - 一次计算，多次使用 - 适合复杂模型

缺点： - 可能计算不需要的世界 - 初期工作量较大

例题：判断 \(M, w_1 \models \Box(\Diamond p \rightarrow \Box q)\)

模型 M:
w1 → w2 → w3 ← w4
p,q    q

步骤1：原子命题真值
w1    w2    w3    w4
p     1     0     0     0
q     1     1     0     1

步骤2：计算 ◇p
w1: Succ={w2}, w2⊭p → w1⊭◇p → 0
w2: Succ={w3}, w3⊭p → w2⊭◇p → 0
w3: Succ={w4}, w4⊭p → w3⊭◇p → 0
w4: Succ={w3}, w3⊭p → w4⊭◇p → 0

步骤3：计算 □q
w1: Succ={w2}, w2⊨q → w1⊨□q → 1
w2: Succ={w3}, w3⊭q → w2⊭□q → 0
w3: Succ={w4}, w4⊨q → w3⊨□q → 1
w4: Succ={w3}, w3⊭q → w4⊭□q → 0

步骤4：计算 ◇p → □q
w1    w2    w3    w4
◇p    0     0     0     0
□q    1     0     1     0
→     1     1     1     1

步骤5：计算 □(◇p → □q)
w1: Succ={w2}, w2⊨(◇p→□q) → w1⊨□(...) → 1 ✓

答案：M, w1 ⊨ □(◇p → □q)  ✓

4.4 两种策略对比

特性	Top-down	Bottom-up
适用场景	简单公式（1-2层嵌套）	复杂公式（3+层嵌套）
思路	递归分解	逐层构建
优点	直观、可提前终止	系统、不易出错
缺点	嵌套深易错	初期工作量大
考试建议	用于解释题	用于计算题

⭐ 考试策略： - 不确定时：用Bottom-up（更安全） - 时间紧时：用Top-down（可能更快） - 两种结合：用Top-down找思路，Bottom-up验证答案

4.5 完整例题1：判断 \(M, w_3 \models \Box \Diamond \Diamond q\)

模型 M:
w1 → w2 ⇄ w3 → w4
p        q

正式定义：

- W = {w1, w2, w3, w4}
- R = {(w1, w2), (w2, w3), (w3, w2), (w3, w4)}
- V(p) = {w1}, V(q) = {w2}

Top-down解法：

目标：M, w3 ⊨ □◇◇q ?

步骤1：找w3的后继
Succ(w3) = {w2, w4}

步骤2：检查 M, w2 ⊨ ◇◇q

步骤2.1：找w2的后继
Succ(w2) = {w3}

步骤2.2：检查 M, w3 ⊨ ◇q
找w3的后继：Succ(w3) = {w2, w4}
检查 M, w2 ⊨ q → w2 ∈ V(q) → ✓
因此 M, w3 ⊨ ◇q  ✓

步骤2.3：因此 M, w2 ⊨ ◇◇q  ✓

步骤3：检查 M, w4 ⊨ ◇◇q

步骤3.1：找w4的后继
Succ(w4) = ∅  (空集！)

步骤3.2：因此 M, w4 ⊭ ◇◇q  ✗
(没有后继，Diamond总为假)

步骤4：结论
不是所有后继都满足 ◇◇q
因此 M, w3 ⊭ □◇◇q  ✗

4.6 完整例题2：判断 \(M, w_3 \models \Box(p \lor \Diamond p)\)

模型 M:
w1 → w2 ⇄ w3
p,q    q

正式定义：

- W = {w1, w2, w3}
- R = {(w1, w2), (w2, w3), (w3, w2), (w3, w1)}
- V(p) = {w1}, V(q) = {w1, w2}

Bottom-up解法：

步骤1：原子命题真值
w1    w2    w3
p     1     0     0
q     1     1     0

步骤2：计算 ◇p
w1: Succ={w2}, w2⊭p → w1⊭◇p → 0
w2: Succ={w3}, w3⊭p → w2⊭◇p → 0
w3: Succ={w2,w1}, w1⊨p → w3⊨◇p → 1

步骤3：计算 p ∨ ◇p
w1    w2    w3
p     1     0     0
◇p    0     0     1
∨     1     0     1

步骤4：计算 □(p ∨ ◇p)
w3: Succ={w2,w1}
M, w2 ⊨ p ∨ ◇p? → 0 ∨ 0 = 0  ✗

    结论：存在后继不满足 p ∨ ◇p
          因此 M, w3 ⊭ □(p ∨ ◇p)  ✗
    ```

---

## 5. 端点的特殊性质（Endpoints）

### 5.1 什么是端点？

**定义**：世界 \(w\) 是**端点（Endpoint）**，当且仅当 \(w\) 没有后继。

**形式化**：
\[
\text{Succ}(w) = \emptyset
\]

**图形表示**：

w1 → w2 → w3
            ↓
            w4  ← 端点（无箭头出去）
```

5.2 端点的性质（⚠️ 重要陷阱）

性质1：对于端点 \(w\)，\(\Box \phi\) 总是为真（对任意公式 \(\phi\)）

推理：

M, w ⊨ □φ
⟺ 对于所有后继 w'，M, w' ⊨ φ
⟺ 对于所有0个后继，M, w' ⊨ φ
⟺ "0个后继都满足φ" → 空虚为真！ ✓

性质2：对于端点 \(w\)，\(\Diamond \phi\) 总是为假（对任意公式 \(\phi\)）

推理：

M, w ⊨ ◇φ
⟺ 存在至少一个后继 w' 使得 M, w' ⊨ φ
⟺ 存在至少1个后继...
⟺ 但w有0个后继 → 0 < 1 → ✗

5.3 端点的极端例子

例子：判断端点 \(w_1\) 的性质

模型 M:
w1  (无箭头出去)

V(p) = ∅  (p在任何世界都不为真)

结论（看似矛盾但逻辑正确）：

1. M, w1 ⊨ □p                ✓  (空虚为真)
2. M, w1 ⊨ □¬p               ✓  (空虚为真)
3. M, w1 ⊨ □(p ∧ ¬p)         ✓  (空虚为真！)
4. M, w1 ⊭ ◇p                ✗  (没有后继)
5. M, w1 ⊭ ◇¬p               ✗  (没有后继)
6. M, w1 ⊭ ◇(p ∨ ¬p)         ✗  (即使p∨¬p是永真式)

⚠️ 考试陷阱： - 不要被"矛盾公式"迷惑！ - \(\Box(p \land \neg p)\) 在端点为真 - 这是逻辑上一致的（虽然违反直觉）

5.4 如何避免端点陷阱

策略： 1. 先检查后继：判断公式前，先确认世界有无后继 2. 记住规则：端点 → Box总真，Diamond总假 3. 不要猜测：严格应用语义规则，不要凭直觉

---

6. 多智能体模态逻辑（预告）

⚠️ 提示：这部分是Week 4-5的内容，这里只做简单预告。

6.1 为什么需要多智能体？

问题：如何表达"我知道你知道 \(p\)"？

尝试1（错误）：\(\Box \Box p\)

问题：这表示"我知道（我知道 \(p\)）"，不是"我知道你知道 \(p\)"

解决方案：为每个智能体使用不同的Box

6.2 多智能体语言

扩展： [ \phi \coloneqq p \mid \neg \phi \mid \phi \land \psi \mid \Box_a \phi ]

其中 \(a \in \mathcal{A}\) 是智能体集合中的一个智能体。

例子： - \(\Box_I p\)："我（I）知道 \(p\)" - \(\Box_Y p\)："你（You）知道 \(p\)" - \(\Box_I \Box_Y p\)："我知道你知道 \(p\)"

6.3 多智能体模型

扩展：\(M = (W, \mathbf{R}, V)\)，其中： - \(\mathbf{R} = \{R_a \mid a \in \mathcal{A}\}\)：每个智能体有自己的关系

图形表示：箭头上标注智能体

模型 M:
w1 --a--> w2
w1 --b--> w3
w2 --a,b--> w3

解释：

- 从w1到w2有a箭头（智能体a的关系）
- 从w1到w3有b箭头（智能体b的关系）
- 从w2到w3有a和b箭头（两个智能体都可达）

语义规则： [ M, w \models \Box_a \phi \iff \text{对于所有 } w' \text{ 使得 } (w, w') \in R_a, \text{ 有 } M, w' \models \phi ]

Week 4-5将详细学习！

---

7. 练习题

Exercise 7.1 - 基础模型检查

给定模型：

    w1 → w2 → w3 → w4
    p         p

- W = {w1, w2, w3, w4}
- R = {(w1, w2), (w2, w3), (w3, w4), (w4, w2)}
- V(p) = {w1, w3}

判断： 1. \(M, w_1 \models p\) 2. \(M, w_2 \models p\) 3. \(M, w_3 \models \Box \neg p\) 4. \(M, w_4 \models \Box \Diamond \neg p\)

答案

1. **True** — \(w_1 \in V(p)\) 2. **False** — \(w_2 \notin V(p)\) 3. **True** — \(w_3\)的唯一后继是\(w_4\)，且\(w_4 \notin V(p)\) 4. **False** — \(w_4\)的唯一后继是\(w_2\)，但\(w_2\)没有后继满足\(\neg p\)（\(w_3 \in V(p)\)）

Exercise 7.2 - Diamond推导

给定模型：

    w1 ⇄ w2
    q      p

用两种方法判断：\(M, w_1 \models \Diamond p\)

方法1：直接应用Diamond规则
方法2：使用定义 \(\Diamond p \equiv \neg \Box \neg p\)

答案

**方法1**： - \(w_1\)的后继：\(\{w_2\}\) - \(M, w_2 \models p\) ✓ - 存在后继满足\(p\)，因此\(M, w_1 \models \Diamond p\) ✓ **方法2**： - \(M, w_1 \models \neg \Box \neg p\) - 需要\(M, w_1 \not\models \Box \neg p\) - 检查\(w_1\)的后继\(w_2\)：\(M, w_2 \not\models \neg p\)（因为\(w_2 \in V(p)\)） - 不是所有后继满足\(\neg p\)，因此\(M, w_1 \not\models \Box \neg p\) ✓ - 因此\(M, w_1 \models \Diamond p\) ✓

Exercise 7.3 - 端点陷阱

给定模型：

    w1 → w2
    p

(w2无后继)

判断（解释原因）： 1. \(M, w_2 \models \Box p\) 2. \(M, w_2 \models \Box \neg p\) 3. \(M, w_2 \models \Diamond p\) 4. \(M, w_2 \models \Diamond \neg p\)

答案

1. **True** — \(w_2\)是端点，\(\Box\)任意公式都为真（空虚为真） 2. **True** — 同理 3. **False** — \(w_2\)是端点，\(\Diamond\)任意公式都为假（没有后继） 4. **False** — 同理

Exercise 7.4 - 复杂嵌套

给定模型：

    w1 → w2 ⇄ w3 → w4
    p,q    q         q

用Bottom-up方法判断：\(M, w_1 \models \Box \Diamond \Box q\)

答案

步骤1：原子命题
w1    w2    w3    w4
q     1     1     0     1

步骤2：计算 □q
w1: Succ={w2}, w2⊨q → w1⊨□q → 1
w2: Succ={w3}, w3⊭q → w2⊭□q → 0
w3: Succ={w2,w4}, w2⊨q,w4⊨q → w3⊨□q → 1
w4: Succ=∅ → w4⊨□q → 1 (端点)

步骤3：计算 ◇□q
w1: Succ={w2}, w2⊭□q → w1⊭◇□q → 0
w2: Succ={w3}, w3⊨□q → w2⊨◇□q → 1

步骤4：计算 □◇□q
w1: Succ={w2}, w2⊨◇□q → w1⊨□◇□q → 1 ✓

答案：True

---

8. 考试重点

8.1 Class Test 1中的模型检查（约30分）

典型题型（基于2019/2022真题）：

第1题：画模型图（5分） - 给定 \(M = (W, R, V)\)，画出图形 - 注意箭头方向、标注原子命题

第2题：解释语义规则（5-7分） - 解释 \(M, w \models \Box \phi\) 的含义 - 给出 \(\Diamond \phi\) 的完整推导

第3题：模型检查（15-18分） - 给定模型和公式，判断是否满足 - 必须解释推理过程（不能只写答案） - 通常3-4个子问题

8.2 答题模板

问题：解释为什么 \(M, w_3 \models \Box(p \lor \Diamond q)\)

答案结构：

1. 应用Box规则
"M, w3 ⊨ □(p ∨ ◇q) 当且仅当
对于所有w3的后继w'，M,w' ⊨ p ∨ ◇q"
2. 找后继
"w3的后继为：{w1, w2}"
3. 逐一检查后继

"检查 M, w1 ⊨ p ∨ ◇q:
    - M, w1 ⊨ p? → w1 ∈ V(p) → ✓
    - 因此 M, w1 ⊨ p ∨ ◇q  ✓"

"检查 M, w2 ⊨ p ∨ ◇q:
    - M, w2 ⊨ p? → w2 ∉ V(p) → ✗
    - M, w2 ⊨ ◇q? → 需要检查w2的后继...
Succ(w2) = {w3}
M, w3 ⊨ q? → w3 ∈ V(q) → ✓
    - 因此 M, w2 ⊨ ◇q  ✓
    - 因此 M, w2 ⊨ p ∨ ◇q  ✓"
4. 得出结论
"所有后继都满足 p ∨ ◇q，
因此 M, w3 ⊨ □(p ∨ ◇q)  ✓"

8.3 常见错误

❌ 错误1：忘记检查所有后继

错误：只检查了w1，忘记w2
正确：必须检查Succ(w3)中的所有元素

❌ 错误2：混淆Box和Diamond

错误：Box需要"至少一个"后继满足
正确：Box需要"所有"后继满足
Diamond需要"至少一个"后继满足

❌ 错误3：端点判断错误

错误：端点w满足 ◇p（因为没后继所以"可能"）
正确：端点w不满足 ◇p（没后继就不可能）

❌ 错误4：省略解释

错误：M, w1 ⊨ □p. Answer: Yes.
正确：必须写出推理步骤（见答题模板）

8.4 必须掌握的技能

技能	重要程度	练习建议
画模型图	⭐⭐⭐⭐⭐	每天画5个
找后继	⭐⭐⭐⭐⭐	确保不遗漏
Box规则应用	⭐⭐⭐⭐⭐	核心中的核心
Diamond推导	⭐⭐⭐⭐⭐	考试必考
端点识别	⭐⭐⭐⭐	常见陷阱
Top-down vs Bottom-up	⭐⭐⭐	灵活选择

8.5 三天复习计划

Day 1（今天，10月25日）： - 记住五大语义规则 - 做Exercise 1.1-1.4（课本） - 确保理解Box和Diamond的区别

Day 2（10月26日）： - 练习Top-down和Bottom-up方法 - 做2019 Class Test 1的模型检查题 - 总结端点陷阱

Day 3（10月27日，考前一天）： - 做2022 Class Test 1的模型检查题 - 模拟考试计时练习（15分钟完成一道大题） - 复习答题模板

---

9. 公式速查表

9.1 核心语义规则

连接词	语义规则
原子	\(M, w \models p \iff w \in V(p)\)
否定	\(M, w \models \neg \phi \iff M, w \not\models \phi\)
合取	\(M, w \models \phi \land \psi \iff M, w \models \phi \text{ 且 } M, w \models \psi\)
Box	\(M, w \models \Box \phi \iff \forall w' \in \text{Succ}(w): M, w' \models \phi\)
Diamond	\(M, w \models \Diamond \phi \iff \exists w' \in \text{Succ}(w): M, w' \models \phi\)

9.2 重要等价式

等价式	名称
\(\Diamond \phi \equiv \neg \Box \neg \phi\)	Diamond定义
\(\Box \phi \equiv \neg \Diamond \neg \phi\)	Box的对偶
\(\Box(\phi \land \psi) \equiv \Box \phi \land \Box \psi\)	Box分配律（合取）
\(\Diamond(\phi \lor \psi) \equiv \Diamond \phi \lor \Diamond \psi\)	Diamond分配律（析取）

⚠️ 不等价： - \(\Box(\phi \lor \psi) \not\equiv \Box \phi \lor \Box \psi\) - \(\Diamond(\phi \land \psi) \not\equiv \Diamond \phi \land \Diamond \psi\)

9.3 端点性质

对于端点 \(w\)（\(\text{Succ}(w) = \emptyset\)）： - \(M, w \models \Box \phi\) 总是True（对任意\(\phi\)） - \(M, w \models \Diamond \phi\) 总是False（对任意\(\phi\)）

---

10. 下周预告

Week 4 将学习： - 有效性判断技巧 - 反例构造方法（如何证明公式不是valid） - 证明系统K基础 - 多智能体模型详细介绍

预习建议： - 完成本周所有练习题 - 确保完全理解Box和Diamond的区别 - 练习快速画模型图

---

笔记完成时间：2025年10月25日 22:01
版本：v1.0（完整版）

质量保证： - ✅ 所有表格和模型图使用代码块格式 - ✅ 基于Lecture 4 + Part 6课件 + 官方练习题 - ✅ 包含Top-down和Bottom-up两种方法 - ✅ 详细的端点性质讲解 - ✅ 多智能体预告 - ✅ 6个详细例题 + 4个练习题 - ✅ 考试导向的答题模板

复习建议： 1. 完全理解五大语义规则 2. 每天练习10道模型检查题 3. 记住端点陷阱 4. 准备Week 4的有效性判断

---

Good luck with your studies! 🎓 ```

---

✅ Week 3笔记生成完毕！

主要特点：

1. ✅ Top-down + Bottom-up两种方法详细讲解
2. ✅ 端点陷阱完整覆盖（您指出的关键点）
3. ✅ 多智能体预告（Lecture 4最后内容）
4. ✅ 6个详细例题 + 4个练习题（带答案）
5. ✅ 所有模型图使用代码块格式
6. ✅ 答题模板和考试策略

请确认：

1. 内容是否全面（对比您提供的自我评估）？
2. Top-down和Bottom-up方法是否清晰？
3. 我现在继续生成Week 4-5笔记吗？ ¹²³⁴

⁂

---

1. COMP304_521-Lecture-4_Zi-Mu-_English-United-Kingdom.txt ↩

2. COMP304.pdf ↩

3. 2_Modal_Logic_Exercises_with_solution.pdf ↩

4. Part_6_modal_logic_semantics_handout.pdf ↩