一阶逻辑与归结推理原理

可视化演示

动态演示一阶逻辑与归结推理原理的核心机制，通过概览/流程/对比/趋势四种模式展示关键概念与交互流程。

谓词逻辑基础

档案室的墙上挂满卡片。命题逻辑的句子只能整句判断真假，像一张只写着一句话的便签：“张三在案发现场”。可侦探要查的是“谁在现场”，便签没法回答。一阶逻辑则是可以拆零部件的语言：它在“张三”和“在案发现场”之间画出连线，让句子变成可以检索、可以组合的零件。

一阶逻辑有三类基本零件：常量（特指对象，如人名“张三”）、变量（泛指对象，如 x）以及谓词（表示对象的属性或对象之间的关系）。此外还有函数，它像“张太太”这样的复合称号一样，返回一个新的对象表达式。在 AI 知识表示里，事实正是用这种“谓词加参数”的形式写进知识库的。

“一阶”的意思是，谓词只能像螺丝一样拧在对象上，而不能拿谓词去修饰另一个谓词。每个陈述句本身有真假值，例如“小柯是侦探”写为 Detective(XiaoKe)。把几条事实组合起来，就可以表达规则：“只要 a 是人且 a 在案发现场，a 就是嫌疑人”：

小柯把口供里的主角们一一做成档案卡：常量是姓名，谓词是卡片上的标签。一张卡片说不清的事，多张卡片叠在一起就构成知识库。这就是命题逻辑做不到、而一阶逻辑可以做的地方——句子可以被拆开、组合，再拿去推理。

量词与表达式

全城协查通报贴满了街道。通报有两类：第一类是“所有目击者都应配合调查”，第二类是“监控里有一个神秘身影”。第一类要覆盖全部个体，第二类只要求确定至少一个。若只用一张张档案卡逐一登记，香港谁都写不完。

一阶逻辑为此设计了两个量词：全称量词 \(\forall x\) 读作“对论域中的每一个 x”，存在量词 \(\exists x\) 读作“论域中至少存在一个 x”。量词决定变量 x 的“管辖范围”，数学上称为辖域。判断一个带量词的句子真假，必须弄清楚量词到底管住了哪一部分。

否定一个带量词的句子时要格外小心：否定号会跨过量词，并且把全称量词翻转为存在量词。“不是所有人都清白”这句话，就是在说“至少有一个不清白的人”：

小柯把协查通报翻译成两条公式，贴进档案系统：全城排查变成“对每个市民套用一条规则”，“神秘身影”则记成“存在一个未知对象”。量词，就是让口供从“点名道姓”升级到“覆盖所有人和某个神秘人”的装置。

合取范式变换

师父立下规矩：所有口供必须统一格式——每一行写成“情况 A 或情况 B 或情况 C”，行与行之间用“并且”连接。小柯手里的卷宗却是东一句“如果……”，西一句“而且……”，根本没法快速比对。把口供改写成这种标准格式的过程，就是合取范式（CNF）变换。

为了执行归结，每个逻辑公式都必须变成 CNF：它是若干个“子句”的合取，每个子句是若干文字（原子公式或原子公式的否定）的析取。归结只认这种结构，就像比对机器只认标准表格。

变换分三步走：先消去蕴含与等值，把“如果 P 那么 Q”换成“¬P 或 Q”；再把否定号一路向里推，直到只贴在原子公式上；最后用分配律把“与”从“或”的括号里拎出来。第三步用到的核心等式：

小柯花了一晚上把十五份口供全部改写成标准行式。原本绕来绕去的表述，变成清一色的“或句的且句”——核对、排序、比对都变成可以交给机械执行的工序。

Skolem标准化

口供里有一句“有一个人递给了凶手一把刀”，可没人看清那人是谁。在逻辑里，“有一个人”就是存在量词。侦探不能追查一个无名氏，于是师父出了个主意：既然不知道名字，就先给他一个临时代号 f(x)，代号由他出现在哪份口供里决定。这个过程叫 Skolem 化。

Skolem 化的前提是前束范式：把所有量词都挪到公式最前面。在这个基础上，对每个存在量词变量 y，用一个全新的函数符号 f 替换它。如果 y 不在任何全称量词的辖域内，就用一个全新常量替换；如果 y 依赖于前面的全称变量 x，就必须用 Skolem 函数 f(x)。

“每个人至少认识一个人”写作 \(\forall x \exists y \mathrm{Knows}(x,y)\)。化去存在量词后得到：

小柯给“神秘人”起了个代号“黑衣人 K”，挂在刀这条线索下。同事们都知道 K 不是真名，只是一个占位符号。Skolem 化就是逻辑世界的“起代号规则”——保证每个存在对象都有可指称的名字，又不额外引入事实。

归结推理规则

两位证人录了口供。甲说：“要么是厨子，要么是管家。”乙说：“厨子不在家。”小柯立刻得出结论：“是管家。”这个动作看似普通，却是整台破案机器的发动机——把两条都提到“厨子”的口供合并，消去互相矛盾的一句，把其余部分拼成新结论。

归结规则在子句层面操作：设有两个子句，一个含有文字 L，另一个含有文字 ¬L，两者互为否定。把这对互补文字同时删去，再把两个子句剩余的文学合并成一个新子句，就得到归结式。这就像两堆积木相撞，正负极相抵的部分消失，剩余零件掉落在一起。

规则用推理式写成：

小柯把这条规则反复使用：两两比对、消去矛盾、生成新口供，再汇入口供池。归结论证就像侦探在证据板上交叉连线，连到尽头时，疑点要么被消去，要么被同一个结论锁死。

合一算法

两份口供都提到“那个人”。甲说：“那个人递了刀。”乙说：“那个人穿了黑风衣。”小柯必须判断，两份口供里的“那个人”是不是同一个人。如果确定是，就做一次替换，把两处“那个人”统一成同一个名称。合一算法干的正是这件事。

归结时，互补文字往往不是字面相同，而是“长得相似但含变量”。比如 P(x) 与 ¬P(a) 并不一致，但只要做替换 \(x \mapsto a\)，两者就完全相同。寻找一个替换使两个表达式一致的动作叫合一，找到的替换称为合一子。

如果存在多种合一方式，要取最具一般性的那一个（MGU，最一般合一）。例如 \(\mathrm{Knows}(x, y)\) 与 \(\mathrm{Knows}(\mathrm{Tom}, z)\) 的最一般合一是：

“确认两个人实际是一个人”是小柯破案的关键一步。合一算法就是逻辑推理里的实名认证：它把散落证据中的变量钉死到同一个身份上，让归结得以继续。

归结反演证明

小柯锁定真凶是管家，但需要严格证明。师父说：用反证法。先假设管家无罪，把这个假设写进口供池——如果这个假设与其他证据推出逻辑矛盾（空子句），就说明“管家无罪”是错的，因此管家必然有罪。

归结反演用于证明“知识库 KB 推出结论 α”。做法是：把 KB 中所有公式化为子句，再把 α 的否定也化为子句，全部放入同一个子句池，不断执行归结。如果最终归结出空子句 □，说明“KB 与 ¬α 同时为真”不可能成立，于是 \(KB \vDash \alpha\)。

整个证明的骨架用推导式表达：

小柯把“管家无罪”假设扔进证据池，几轮交叉比对后，池里推出了“空话”——整个假设无法自洽。他在证据板上画下一个大大的 □：“假设不成立，真相只有一个。”归结反演，就是用矛盾来证明真理。

应用与局限性

这套破案法很快在小柯手里走红，但师父提醒他：案件材料一旦变厚，两两比对的组合数量会爆炸式增长。再厉害的侦探，也会在堆积如山的口供前卡壳。归结能为自动定理证明提供机械引擎，但具体先比哪两份口供、怎么控制搜索方向，仍需要策略。

在真实世界里，归结思想以各种形态出现在定理证明器、程序验证工具和逻辑编程语言中。归结法之所以可靠，在于两个数学性质：可靠性——推出的结论必然为真；完备性——为真的结论必然能被推出。完备性可以写成一个漂亮的充要条件：

小柯最终结案，也明白了侦探的边界：归结推理是强大的机械引擎，但面对大型真实问题，必须借助支撑集策略、文字消去、DPLL 风格搜索等手段控制组合爆炸。一阶逻辑能说清的世界很大，推理成本也随之上升——知道工具能做什么、做不到什么，才是一名合格的逻辑侦探。

AI 应用场景

Python 演示

# -*- coding: utf-8 -*-"""迷你归结推理器：用归结反演自动证明 KB 能否推出 goal"""from itertools import product  def negate(literal):    """返回一个字面量的否定：cat <-> ~cat"""    return literal[1:] if literal.startswith('~') else '~' + literal  def resolve(c1, c2):    """对两个子句执行一次归结：找互补文字对，消去后合并剩余文字"""    results = []    for l1, l2 in product(c1, c2):        if l1 == negate(l2):            resolvent = (c1 - {l1}) | (c2 - {l2})            if resolvent not in results:                results.append(resolvent)    return results  def refute(kb, goal):    """归结反演：把目标否定加入子句池，反复两两归结直到出现空子句"""    pool = [frozenset(c) for c in kb + [{negate(goal)}]]    seen = set(pool)    trace = []     for _ in range(100):        grown = list(pool)        for i in range(len(pool)):            for j in range(i + 1, len(pool)):                for r in resolve(pool[i], pool[j]):                    if not r:                        trace.append((pool[i], pool[j], frozenset(), '空子句'))                        return True, trace                    if r not in seen:                        seen.add(r)                        grown.append(r)                        trace.append((pool[i], pool[j], r, '新子句'))        if len(grown) == len(pool):            break        pool = grown    return False, trace  if __name__ == '__main__':    # 知识库：小咪是猫；猫都是哺乳动物（用 ~Cat ∨ Mammal 表示蕴含）    kb = [{'Cat'}, {'~Cat', 'Mammal'}]    ok, steps = refute(kb, 'Mammal')    print('定理成立!' if ok else '无法证明此结论')    for a, b, c, tag in steps:        print('%s + %s -> %s %s' % (set(a), set(b), set(c), tag))

1. return literal[1:] if literal.startswith('~') else '~' + literal求一个文字的否定形式，构成互补对的前提。
2. for l1, l2 in product(c1, c2)枚举两个子句的所有文字组合，寻找互为否定的那一对。
3. resolvent = (c1 - {l1}) | (c2 - {l2})核心归结动作：删掉互补文字，把剩余文字合并成新子句。
4. pool = [frozenset(c) for c in kb + [{negate(goal)}]]反演的关键第一步：先把结论的否定放进子句池。
5. if not r:空子句出现，表示矛盾爆发，定理得证。
6. if len(grown) == len(pool): break没有新子句产生时终止，说明当前证据不足，推不出结论。

常见误区

面试题