2.1 命题逻辑、Horn 规则与一阶表示：推导成立不等于事实为真

“地面湿了，所以昨夜一定下雨。”这句话把一个可能原因当成了唯一原因。Rain → Wet 与 Wet 不能推出 Rain；洒水器、漏水或清洁同样能让地面湿。逻辑检查得出推理有误，至于谁忘了关水龙头，还得另查。

知识系统需要同时区分：世界中的事实、语言中的句子、知识库的假设，以及推理规则允许推出什么。

本课目标

• 区分语法、解释、模型、蕴含与推导；
• 正确使用 implication、modus ponens 与 contraposition；
• 用 Horn clause 实现带多前件和证明记录的前向链；
• 理解一阶逻辑的变量、量词、谓词与 unification 边界。

1. 语法与语义是两层

命题逻辑中的原子命题，如 Rain、Wet，在某个解释下取真或假。连接词定义复合句：

• $\mathrm{\neg }P$：非；
• $P\wedge Q$：且；
• $P\vee Q$：或（通常是包含性或）；
• $P\to Q$：若 P 则 Q；
• $P\leftrightarrow Q$：当且仅当。

知识库 $KB$ 蕴含句子 $\alpha$，写作 $KB\models \alpha$：所有让 $KB$ 为真的解释也让 $\alpha$ 为真。这是语义关系。

推理系统写作 $KB⊢\alpha$，表示按某套形式规则可推导 $\alpha$。它是否可靠取决于：

• soundness：能推出的都被语义蕴含；
• completeness：被语义蕴含的都能推出（相对于语言/证明系统）。

输入事实可能错误、规则可能不适用于当前领域。形式推导正确不证明知识库准确。

2. Implication 容易被自然语言误导

由 $P\to Q$ 和 $P$ 推出 $Q$ 是 modus ponens。

由 $P\to Q$ 和 $\mathrm{\neg }Q$ 推出 $\mathrm{\neg }P$ 是否定后件式（modus tollens）。逆否等价（contraposition）则指 $P\to Q$ 与 $\mathrm{\neg }Q\to \mathrm{\neg }P$ 在经典逻辑中等价。

下面两种不成立：

• 肯定后件：$P\to Q,Q\therefore P$；
• 否定前件：$P\to Q,\mathrm{\neg }P\therefore \mathrm{\neg }Q$。

“如果下雨，地湿”没有说“只有下雨才湿”。若业务真正想表达双向条件，要明确写出充分与必要条件，并验证例外。

3. Horn clause 让规则推理可执行

一条 definite Horn rule 可写成：

$$p_1\wedge p_2\wedge \cdots \wedge p_k\to q.$$

前向链从事实出发，只有当全部前件已知时才加入结论。下面是 Python 3.9+ 函数片段（partial），输入为字符串事实和有限 Rule 集合。missing 统计尚未从队列传播的前件数，每个事实只传播一次；空前件规则直接作为事实播种。计数方法可对照 Berkeley CS 188 的前向链示例。

from collections import defaultdict, deque
from dataclasses import dataclass

@dataclass(frozen=True)
class Rule:
    premises: frozenset[str]
    conclusion: str
    rule_id: str

def forward_chain(initial_facts, rules):
    rules = list(rules)
    known = set(initial_facts)
    proof = {fact: ("given", ()) for fact in known}
    waiting = defaultdict(list)
    missing = {}

    for i, rule in enumerate(rules):
        missing[i] = len(rule.premises)
        for premise in rule.premises:
            waiting[premise].append(i)

    agenda = deque(sorted(known))
    fired = set()
    for i, rule in enumerate(rules):
        if not rule.premises:
            fired.add(i)
            if rule.conclusion not in known:
                known.add(rule.conclusion)
                proof[rule.conclusion] = (rule.rule_id, ())
                agenda.append(rule.conclusion)

    while agenda:
        fact = agenda.popleft()
        for i in waiting[fact]:
            missing[i] -= 1
            if missing[i] == 0 and i not in fired:
                fired.add(i)
                rule = rules[i]
                if rule.conclusion not in known:
                    known.add(rule.conclusion)
                    proof[rule.conclusion] = (
                        rule.rule_id,
                        tuple(sorted(rule.premises)),
                    )
                    agenda.append(rule.conclusion)

    return known, proof

例如初始事实 {A}，规则 A→B、A∧B→C 应得到 {A,B,C}。只有 {A} 而缺少 B 的多前件规则不能提前触发；没有初始事实但存在 True→A 时，仍应推出 A。若先从计数中扣掉已知事实，又在出队时再扣一次，就会漏推或误推。

证明记录让系统回答“为什么”。生产实现还需处理规则版本、事实来源、时间有效性、撤回和冲突；单调前向链只会增加事实，不能自然撤销旧结论。

4. Closed-world 与 open-world

Open-world assumption：知识库没有 P，不表示 ¬P。适合知识不完整的场景。

Closed-world assumption：查询不到 P 时按假处理，常见于受控、完整性有保证的数据库/逻辑程序。

两种假设的区别在于：缺失记录是否足以支持否定判断。

例如设备登记库有完整资产清单时，“查不到设备”可触发不存在判断；公开知识图谱查不到某人的证书，不能断言此人没有证书。

5. Backward chaining 从目标找前提

后向链要证明 Slippery，查找以它为结论的规则，再递归证明其前件。它适合目标较少的查询，却要处理：

• 多条可选规则；
• 循环依赖；
• 重复子目标；
• 变量替换；
• 深度与资源限制。

Memoization/tabling 可避免相同子目标反复证明，并帮助处理某些递归规则。

6. 命题符号不能复用结构

若要表达：

所有需要救援且位置已知的队伍都应派遣支援
team-7 需要救援
team-7 的位置已知

为每个队伍手写不同命题会膨胀。一阶逻辑加入：

• 常量：team_7；
• 变量：x；
• 谓词：NeedsRescue(x)；
• 函数：LocationOf(x)；
• 全称/存在量词：$\mathrm{\forall },\mathrm{\exists }$。

规则可写成：

$$\mathrm{\forall }x(NeedsRescue(x)\wedge LocationKnown(x)\to Dispatch(x)).$$

7. Unification 匹配结构

Unification 寻找 substitution 使两个表达式相同，例如：

NeedsRescue(x)
NeedsRescue(team_7)

得到 {x ↦ team_7}。它不是模糊字符串匹配；谓词元数、常量、嵌套项和 occurs check 都影响正确性。

通用一阶逻辑推理可半判定且成本很高。Datalog 等受限语言通过禁止任意函数项、采用安全规则等方式换取可终止/可实现的查询性质。选择表示语言时要在表达力、可判定性和解释成本间取舍。

8. 冲突、时间与默认规则

现实规则常出现：

状态=完成 → 可结算
存在未解决争议 → 不可结算

经典逻辑中同时得到命题与其否定会造成不一致。工程系统需定义：

• 规则优先级是否有领域依据；
• 默认规则遇到例外怎样撤回；
• 事实的有效时间和观察时间；
• 冲突是阻断、升级还是采用 paraconsistent reasoning；
• 谁有权修正规则和事实。

不要把 if/elif 的代码顺序偷偷当作政策优先级。

常见误区

• 地湿可以反推下雨：这是肯定后件。
• 可推导就证明现实为真：只能证明相对于知识库和规则成立。
• 前向链等于一串 if：还需多前件、饱和、循环和证明来源。
• 没记录就等于否定：取决于世界假设和数据完整性。

练习

1. 为四种 implication 推理各构造一个有效或无效例子。
2. 给前向链加入多前件规则，输出完整证明树。
3. 比较证书库在 open-world 与 closed-world 下的查询结果。
4. 把三个队伍的重复命题改写为一阶谓词与规则。

小结

知识表示决定哪些结构能够被说清，推理规则决定哪些结论可以被证明。逻辑给的是相对于假设的保证，不负责替你验证输入事实或现实机制。

下一课把“证明命题”换成“同时满足一组约束”：排班、着色和数独都可以视为 CSP，但性能取决于传播和搜索顺序。