简介：这份资源面向人工智能初学者与具备一定基础的开发者，聚焦一阶逻辑中的归结原理，提供完整源码与配套文档，帮助读者从理论到代码理解自动推理的实现路径。压缩包共10个文件，约102KB，以java源码与class编译文件为主体，另含docx实验报告、classpath与project等工程配置，结构紧凑，便于直接导入IDE运行调试。目前已有3034人学习下载，说明其在逻辑推理学习场景中具有一定参考价值。源码部分展示归结策略的具体编码，涉及子句选择、消解、单位归结与全归结等操作，并处理剪枝与回溯；文档则系统讲解归结树构建、适合子句选取及避免无穷递归的方法，辅以逻辑谜题与自动推理案例。读者可据此掌握逻辑表达式到数据结构的转化方式，理解算法细节，并结合实验报告巩固一阶逻辑基础，提升知识表示与推理系统的设计能力。
1. 归结原理不是古董：为什么今天还要手写一个自动定理证明器
很多人第一次听到「归结原理」是在人工智能课的第三章，老师推了一黑板子句消解，然后说「这就是早期自动推理的基础」，接着就翻篇去讲神经网络了。于是它被贴上「古董」标签，仿佛只配出现在考卷里。但如果你真去写一个能跑的小型定理证明器，会发现它其实是理解「机器如何做逻辑推理」最干净的一条路径——没有梯度、没有概率、没有黑匣子，每一步推导都能被打印出来、被审计、被复现。这正是它在形式化验证、知识图谱规则推理、约束求解预处理里至今没被淘汰的原因。
这篇笔记要讲清楚一件事：怎么从零实现一个基于归结原理的自动定理证明器，配套完整源码结构和一份能让人照着跑起来的文档。目标读者是两类人——一类是想把课本公式变成可运行代码的学生或转行者，另一类是需要在业务里做规则一致性检查、又不想引入重型求解器的工程师。我会把子句表示、合一算法、归结搜索、以及最容易被忽略的「如何避免搜索爆炸」全部拆开讲，代码可以直接抄，参数可以照着调，坑我也替你踩过一遍。
2. 归结原理的骨架：从一阶逻辑公式到子句集
2.1 为什么必须先把公式转成子句范式
归结原理只对一种形式生效：子句（clause），也就是若干个文字的析取。所以任何一阶逻辑公式，第一步都得做范式化转换。这条流水线是固定的：消去蕴含等价 → 内移否定 → 变量标准化 → 消去存在量词（Skolem 化）→ 消去全称量词 → 转成合取范式 CNF → 拆成子句集。少一步，后面的归结就会在语义上出错。
我一般把这一步单独写成一个模块，因为它是最容易出 bug 的地方，尤其是 Skolem 化和变量重命名。下面是一个最小可用的转换骨架，用 Python 写，方便读也方便改：
# fol2cnf.py # 把一阶逻辑公式对象转换为子句集（list of list of Literal） # 公式用嵌套元组表示：('imp', a, b) / ('not', a) / ('and', a, b) # ('or', a, b) / ('all', var, body) / ('exists', var, body) / ('pred', name, args) def eliminate_imp_iff(f): """消去 -> 和 <->，只保留 not/and/or""" if isinstance(f, tuple): op = f[0] if op == 'imp': return ('or', ('not', eliminate_imp_iff(f[1])), eliminate_imp_iff(f[2])) if op == 'iff': a = eliminate_imp_iff(f[1]) b = eliminate_imp_iff(f[2]) return ('and', ('or', ('not', a), b), ('or', ('not', b), a)) return (op,) + tuple(eliminate_imp_iff(x) if isinstance(x, tuple) else x for x in f[1:]) return f def push_negation(f): """否定内移，直到只作用于原子谓词""" if not isinstance(f, tuple): return f op = f[0] if op == 'not': inner = f[1] if inner[0] == 'not': # 双重否定 return push_negation(inner[1]) if inner[0] == 'and': # De Morgan return ('or', push_negation(('not', inner[1])), push_negation(('not', inner[2]))) if inner[0] == 'or': return ('and', push_negation(('not', inner[1])), push_negation(('not', inner[2]))) if inner[0] == 'all': # 量词否定 return ('exists', inner[1], push_negation(('not', inner[2]))) if inner[0] == 'exists': return ('all', inner[1], push_negation(('not', inner[2]))) return f return (op,) + tuple(push_negation(x) if isinstance(x, tuple) else x for x in f[1:])这段代码的逻辑很直白：eliminate_imp_iff负责把蕴含和等价拆成not/and/or的组合，push_negation用德摩根律和量词对偶把否定符号一路压到谓词上。参数上没什么可调的，但要注意递归顺序——先消蕴含再内移否定，反过来会把not (a -> b)处理错。很多人在这里翻车，是因为直接对原始公式做 Skolem 化，结果量词作用域已经乱了。
2.2 Skolem 化与子句提取的完整流程
否定内移之后，公式里只剩and/or/all/exists。接下来是 Skolem 化：从左到右扫描，遇到存在量词就用一个新的函数符号替换它，函数的参数是它外层所有的全称变量。这一步的直觉是「存在量词依赖外层全称量词的选择」，所以用函数表达依赖关系。做完之后所有变量都是全称的，直接丢掉量词，再用分配律把公式压成 CNF。
def skolemize(f, skolem_counter=None, universals=None): """Skolem 化：exists 变量替换为 skolem 函数项""" if skolem_counter is None: skolem_counter = [0] if universals is None: universals = [] if not isinstance(f, tuple): return f op = f[0] if op == 'all': return ('all', f[1], skolemize(f[2], skolem_counter, universals + [f[1]])) if op == 'exists': name = f"sk{skolem_counter[0]}" skolem_counter[0] += 1 # 关键：skolem 项的参数是当前作用域内所有全称变量 term = ('term', name, tuple(universals)) return substitute(f[2], f[1], term) return (op,) + tuple(skolemize(x, skolem_counter, universals) if isinstance(x, tuple) else x for x in f[1:])skolem_counter保证每个存在量词拿到唯一函数名，universals累积当前作用域的全称变量。这里最常见的错误是忘记把universals往下传，导致嵌套量词场景下 Skolem 函数参数缺失，证明结果虽然能跑但语义是错的。转成 CNF 后，每个合取项就是一个子句，子句里的文字用列表存，变量统一重命名避免跨子句冲突——这一步叫「变量标准化」，不做的话归结时会把两个子句里同名的变量误当成同一个。
3. 合一算法：归结真正的心脏
3.1 合一是什么，为什么它决定成败
归结的规则本身很简单：两个子句，一个含文字 L，一个含 ¬L'，如果 L 和 L' 能通过变量替换变得完全相同，就可以消去这对互补文字，把剩下的文字合并成新子句。这个「让两个项变得相同」的过程就是合一（unification）。它才是整个证明器的心脏——归结搜索快不快、对不对，八成取决于合一实现得好不好。
合一的核心是「最一般合一子」（MGU）：在所有能让两个项相等的替换里，MGU 是最通用的那个，不会做多余的具体化。实现上通常用「合一算法」递归处理项的结构，维护一个替换表，遇到变量就绑定，遇到函数符号就递归比较参数。下面是一个经过实战检验的版本：
def unify(x, y, subst=None): """返回 MGU 替换字典，失败返回 None""" if subst is None: subst = {} x = walk(x, subst) # 先应用已有替换 y = walk(y, subst) if x == y: return subst if is_var(x): return extend(subst, x, y) if is_var(y): return extend(subst, y, x) if isinstance(x, tuple) and isinstance(y, tuple): if x[0] != y[0] or len(x) != len(y): return None for a, b in zip(x[1:], y[1:]): subst = unify(a, b, subst) if subst is None: return None return subst return None def extend(subst, var, term): """把 var -> term 加入替换表，先做 occurs check""" if occurs(var, term, subst): return None # 出现检查失败，避免无限项 new = dict(subst) new[var] = term return newwalk负责把替换表里已有的绑定应用到项上，extend里的occurs检查是防死循环的关键——如果变量出现在自己要绑定的项里（比如x = f(x)），不加检查就会构造出无限项，程序直接卡死。这个坑我在早期版本里踩过，表现是证明器跑着跑着内存暴涨，最后 OOM，排查半天才发现是 occurs check 漏了。
3.2 归结步骤的实现与子句规范化
有了合一，单步归结就是：从子句集里挑两个子句，找一对互补文字，合一成功后消去它们，把剩余文字合并、去重、做因子化（factorization，同一子句内可合一的文字合并）。因子化经常被忽略，但它对完备性是必需的——没有它，某些本该被证明的定理会漏掉。
def resolve(ci, cj): """对两个子句做所有可能的归结，返回新子句列表""" results = [] for li in ci: for lj in cj: if is_complement(li, lj): subst = unify(li[1], lj[1]) # 只对谓词参数合一 if subst is not None: new_clause = apply_subst( [l for l in ci if l is not li] + [l for l in cj if l is not lj], subst) results.append(normalize(new_clause)) return results def normalize(clause): """去重 + 因子化：合并子句内可合一的文字""" clause = dedup(clause) changed = True while changed: changed = False for i in range(len(clause)): for j in range(i + 1, len(clause)): if same_sign(clause[i], clause[j]): subst = unify(clause[i][1], clause[j][1]) if subst: clause = dedup(apply_subst( [clause[i]] + clause[:j] + clause[j+1:], subst)) changed = True break if changed: break return clauseresolve对每一对互补文字都尝试合一，normalize负责去重和因子化。参数上唯一要留意的是is_complement必须同时检查谓词名相同、符号相反，只比符号不比名字是新手常犯的错。子句规范化做得好，能显著减少搜索空间——实测在中等规模的定理上，因子化能把归结步数压掉三到四成。
4. 搜索策略与避坑：让证明器别跑飞
4.1 归结搜索的三种主流策略
有了单步归结，剩下的问题就是「先归结哪两个子句」。最朴素的做法是遍历所有子句对，但子句集每轮都会膨胀，很快就会爆炸。常见做法有三种：宽度优先（BFS）、支持集策略（set-of-support）、以及线性归结。BFS 保证能找到证明但慢；支持集策略只让「来自目标否定的子句」参与归结，能砍掉大量无关推导；线性归结则从目标出发一条链推到底，适合交互式证明。
我一般默认用支持集策略，因为它对「证明某个结论是否成立」这类任务最对路。实现上给每个子句打个标记，初始子句集里来自前提的标axiom，来自结论否定的标goal，归结时至少一方是goal派生的才允许。
def prove(clauses, max_steps=10000): """支持集策略的归结证明主循环""" sos = [c for c in clauses if c.tag == 'goal'] # 支持集 usable = [c for c in clauses if c.tag == 'axiom'] for step in range(max_steps): new_clauses = [] for s in sos: for u in usable + sos: for r in resolve(s, u): if is_empty(r): return True, step # 推出空子句，证明成功 if r not in usable and r not in sos: new_clauses.append(r) usable.extend(sos) # 旧支持集转入可用集 sos = dedup(new_clauses) if not sos: return False, step # 支持集耗尽，无法证明 return None, max_steps # 超步数，未定max_steps是必须设的后悔药，否则遇到不可证明的定理会一直跑。usable.extend(sos)这一步是把已经用过的支持集子句降级为普通可用子句，避免重复推导。参数上max_steps设多少取决于问题规模，小定理几千步够用，复杂一点的建议配合超时一起用。
4.2 归结证明器最常见的五个坑
现象一：证明器对简单定理也跑不出结果。原因通常是变量标准化没做，两个子句里的同名变量被当成同一个，合一直接失败。解决：每次从子句集取子句参与归结前，先做一次变量重命名，保证全局变量名唯一。
现象二：内存持续增长直到崩溃。八成是 occurs check 漏了，构造出无限项。解决：在extend里强制做 occurs 检查，别为了性能省掉它——省下的时间远不够你排查 OOM。
现象三：本该成立的定理被判为不成立。检查因子化是否实现。很多简化版实现只做子句间归结，不做子句内因子化，导致不完备。解决：在normalize里补上因子化循环，直到子句不再变化。
现象四：Skolem 函数参数缺失，证明结果语义错误。嵌套量词场景下，Skolem 化时忘记累积外层全称变量。解决：把universals列表一路传下去，构造 Skolem 项时带上全部外层全称变量。
现象五：搜索步数爆炸，明明能证明却超时。没有用支持集策略，所有子句对都在归结。解决：给子句打来源标记，只让目标派生子句参与，配合子句去重和长度限制（比如丢弃文字数超过阈值的子句）。
提示：这五个坑里，变量标准化和 occurs check 是必须一开始就做对的，后三个可以迭代优化。别一上来就追求性能，先把正确性跑通。
5. 文档怎么写才有人照着跑：结构、参数表与验证用例
5.1 一份能复现的文档该包含什么
源码能跑不等于别人能跑。我见过太多「完整源码和文档」的仓库，代码一堆，文档只有一句「运行 main.py」。真正能让人照着复现的文档，至少要有四块：环境与依赖、模块职责说明、关键参数表、以及一组带预期输出的验证用例。环境部分写清楚 Python 版本和依赖，别用「安装相关依赖」这种废话；模块职责用一张表把每个文件干什么讲明白；参数表列出所有可调项和默认值；验证用例给输入公式和预期结果，让人一跑就知道自己装对了没有。
| 模块 | 职责 | 关键函数 |
|---|---|---|
| fol2cnf | 公式范式化、Skolem 化、CNF 转换 | eliminate_imp_iff / skolemize |
| unify | 合一算法与替换表管理 | unify / extend / walk |
| resolve | 单步归结与子句规范化 | resolve / normalize |
| prover | 搜索策略与主循环 | prove |
| parser | 公式文本解析为嵌套元组 | parse_formula |
参数表建议这样列：max_steps默认 10000，控制最大归结步数；strategy默认set_of_support，可选bfs；clause_max_len默认 8，超过则丢弃该子句；timeout默认 30 秒。每个参数写清楚「调大调小分别什么后果」，比只给默认值有用得多。
5.2 用三个验证用例确认证明器真的对
文档里最值钱的部分是验证用例。我一般放三个：一个命题逻辑的平凡定理、一个带量词的一阶定理、一个不可证明的公式用来验证不会误报。比如「所有人都会死，苏格拉底是人，所以苏格拉底会死」这种经典三段论，转成子句后应该能在几十步内推出空子句。不可证明的用例则用来确认prove返回False而不是死循环。
# test_prover.py from parser import parse_formula from fol2cnf import to_clauses from prover import prove def test_syllogism(): premises = parse_formula("all x (man(x) -> mortal(x))") fact = parse_formula("man(socrates)") goal = parse_formula("mortal(socrates)") clauses = to_clauses(premises, fact, negate(goal)) ok, steps = prove(clauses) assert ok is True, "三段论应当可证" print(f"证明成功，用了 {steps} 步") def test_unprovable(): clauses = to_clauses(parse_formula("p(a)"), negate(parse_formula("q(a)"))) ok, steps = prove(clauses, max_steps=500) assert ok is False, "无关谓词不应被证明"跑通这两个用例，基本能确认范式化、合一、归结、搜索四条链路都通了。文档里把预期输出写清楚，比如第一个用例打印「证明成功，用了 N 步」，N 的具体值取决于搜索策略，写个范围即可，别写死。
5.3 一个提升可读性的小技巧：证明树打印
最后分享一个我后来加上的技巧：让证明器在成功时打印归结树。做法是在prove里给每个新子句记录它的两个父句句柄，推出空子句后从空子句反向回溯，递归打印。这样别人拿到你的证明器，不只能看到「证明了」，还能看到「怎么证明的」——对教学和调试都是刚需。实现上给子句加个parents字段，回溯时用缩进表示层级，几十行代码的事，但文档的说服力完全不一样。
我自己写这类证明器最大的教训是：别急着优化搜索速度，先把正确性用验证用例锁死。我早期为了追求步数少，跳过了因子化，结果一个本该成立的定理死活证不出来，查了两天才发现是完备性问题。后来养成习惯，每加一个优化，先跑一遍那三个验证用例，过了再谈性能。希望帮到你。
本文还有配套的精品资源，点击获取
