逻辑推理与知识表示

逻辑推理与知识表示是符号主义 AI 的第二个分支：用形式化的符号体系表示知识，并通过推理规则从已有知识推导新知识。它是符号主义 AI 的理论基石——搜索与规划解决”怎么做”，逻辑与知识表示解决”知道什么”以及”怎么从已知推出新知”。

核心直觉

知识表示（Knowledge Representation，将世界知识编码为计算机可处理的形式化结构）就是给世界建模型。有两种根本不同的建模方式：

形式逻辑（Formal Logic）= 像写数学证明——“所有人都会死（前提），苏格拉底是人（事实），所以苏格拉底会死（结论）“。严谨、可验证，每一步推理都有数学保证，但要把所有知识写成公式，知识获取成本极高。
语义网络（Semantic Network）= 像画思维导图——节点是概念，边是关系（“鸟—是一种—动物”），顺着边就能推理（“鸟会飞吗？”→ 查”鸟”的属性）。直观、易于理解，但缺乏严格的推理语义。

这两种方式合起来回答了一个核心问题：怎么把人类头脑中的知识存进计算机，还能用来自动推理？ 这个问题的难度在于：人类知识既有严谨的逻辑结构（数学定理），又有模糊的关联结构（“鸟通常会飞，但企鹅不会”）。前者适合形式逻辑，后者适合语义网络——因此符号主义 AI 发展出了两条互补的技术路线。

一个关键区分：知识表示 vs. 知识推理。 表示（representation）解决”知识以什么形式存储”——是写成逻辑公式还是画成图？推理（reasoning）解决”如何从已有知识得出新结论”——是逐条匹配规则还是沿图遍历？两者相互依存：好的表示方式让推理更高效，强大的推理引擎能挖掘表示中隐含的知识。

原理图解

语义网络

语义网络用”节点—边—节点”的图来表示知识，核心思想是属性继承（Inheritance，子概念自动继承父概念的所有属性）——查询”企鹅有没有翅膀”时，不必为每种鸟逐一存储，沿 is-a 边向上查到”鸟”即可获得”有翅膀”。查询时沿着边做推理：

注意”企鹅”节点同时连接”鸟”和”不会飞”——这就是继承 + 异常的表示：企鹅继承了鸟的”有翅膀”，但覆盖了”会飞”。现实世界知识中的例外处理，是语义网络和后来知识图谱的核心挑战。

正向链接推理

拿已知事实去匹配规则前提，命中就推出新事实，循环往复直到没有新结论：

动手实践：正向链接推理机

用 Python 实现一个基于 if-then 规则的正向链接推理引擎：

# 知识库：条件集合 → 结论
rules = [
    ({"产奶"}, {"哺乳动物"}),              # 规则 1
    ({"有毛发"}, {"哺乳动物"}),            # 规则 2
    ({"哺乳动物", "吃肉"}, {"食肉动物"}),   # 规则 3
    ({"食肉动物", "黄褐色", "有条纹"}, {"老虎"}),  # 规则 4
]

def forward_chain(facts: set, rules: list) -> set:
    """正向链接：反复扫描规则，用已知事实推出新事实"""
    changed = True
    while changed:
        changed = False
        for conditions, conclusions in rules:
            # 条件全部满足，且结论尚未推出
            if conditions.issubset(facts) and not conclusions.issubset(facts):
                facts |= conclusions       # 将新结论加入事实集
                changed = True
    return facts

# 测试：观察到的特征
facts = {"有条纹", "黄褐色", "产奶", "吃肉"}
result = forward_chain(facts, rules)
print("老虎" in result)  # True — 推理机推出了"老虎"

这个推理模式正是专家系统的核心。改变规则库就能诊断疾病、配置计算机、审批贷款——推理机本身不变。

知识表示的两条路线

路线	代表方法	特点
形式逻辑	命题逻辑、一阶谓词逻辑、Prolog	严谨，可自动定理证明，但知识获取成本高
结构化表示	语义网络、框架、描述逻辑、本体	直观，适合大规模知识库，演化为今天的知识图谱

实践要点

知识表示的瓶颈不在表示方式，而在知识获取——把领域专家的知识翻译成规则/公理，耗时且易错。
Prolog 是最经典的逻辑编程语言：你声明”事实”和”规则”，Prolog 自动帮你做推理。今天虽然在 AI 主流中不常见，但在特定领域（形式验证、数据库查询语言 Datalog）仍在使用。
**本体（Ontology）**是结构化表示的集大成者——用 OWL 等语言定义”世界上有哪些实体、它们之间有什么关系”，是知识图谱的理论基础。

典型应用

科研与工程验证

自动定理证明：Coq、Lean、Isabelle 等证明助手被数学家和软件工程师用于形式化验证——Lean mathlib 库已形式化了大量现代数学定理，Peter Scholze 的凝聚态数学定理用 Lean 验证通过，证明了人工证明的正确性。
硬件形式验证：芯片设计公司（Intel、AMD、NVIDIA）用 SAT/SMT 求解器（如 Z3）验证电路逻辑的正确性，确保芯片流片前没有逻辑 bug，一次验证可处理数百万个逻辑门级别的约束。

数据与业务系统

数据库查询优化：PostgreSQL、Oracle 等关系数据库的查询优化器使用基于规则的逻辑推理来选择最优执行计划——决定先做哪张表的连接、用哪个索引，直接影响查询性能几个数量级。
业务逻辑验证：Datalog 语言（Prolog 的子集）被用于程序分析（如 Semmle 的代码安全扫描），通过声明式规则自动检测代码中的安全漏洞和反模式，GitHub CodeQL 的底层查询引擎即为 Datalog 实现。

典型类库与工具

类库	语言	说明
SWI-Prolog	Prolog	最成熟的开源逻辑编程语言，声明事实与规则后自动合一与回溯推理
Z3	C++/Python	微软的 SMT 求解器，用于自动定理证明与约束逻辑问题
Lean	C++/Lean	交互式定理证明助手，被数学家用于形式化验证现代数学定理
Coq	OCaml	经典证明助手，支持依赖类型的形式化证明，软件验证领域的学术标准
CodeQL (Datalog)	Datalog	GitHub 的代码分析引擎，底层用 Datalog（Prolog 子集）声明式规则检测代码漏洞
Protégé	Java（桌面应用）	斯坦福的本体编辑器，用 OWL 描述逻辑构建本体与知识库

术语表

术语	英文	解释
一阶逻辑	First-Order Logic (FOL)	包含量词（ $\forall\forall / \exists\exists$ ）和谓词的形式逻辑体系，是符号推理的理论基础
合一	Unification	将两个逻辑项中的变量赋值使它们相等的过程，是 Prolog 推理的核心机制
归结	Resolution	Robinson 1965 提出的推理规则，通过消解互补文字推出新子句，是自动定理证明的基础
谓词逻辑	Predicate Logic	用谓词表示对象属性和关系的逻辑系统，如”人(苏格拉底)“表示”苏格拉底是人”
本体	Ontology	对领域中实体类型、属性及关系的形式化描述，是知识图谱与语义网的理论基础
语义网络	Semantic Network	用节点（概念）和边（关系）表示知识的图结构，是知识图谱的前身
描述逻辑	Description Logic	一阶逻辑的可判定子集，用概念和角色描述知识，是 OWL 的直接理论基础
Horn 子句	Horn Clause	至多一个正文字的析取式，是 Prolog 逻辑程序的推理单元