数理逻辑基础

数理逻辑是符号 AI 的数学根基。符号主义的核心信念是"智能即符号操作"，而逻辑学提供了操纵符号的严格规则。理解命题逻辑和谓词逻辑，是理解后续知识表示、推理引擎、专家系统等内容的前提。

命题逻辑

命题逻辑（Propositional Logic）是最简单的逻辑系统，处理的是可以判断真假的命题。一个命题就是一句话，比如"今天是星期一"或者"服务器正在运行"，它要么为真要么为假，不存在中间状态。

逻辑连接词

命题逻辑通过连接词将简单命题组合成复杂命题。五个基本连接词构成了命题逻辑的全部表达力：

• 否定（$\mathrm{\neg }$）：取反，$\mathrm{\neg }P$ 表示"P 不成立"
• 合取（$\wedge$）：逻辑与，$P\wedge Q$ 表示"P 且 Q"
• 析取（$\vee$）：逻辑或，$P\vee Q$ 表示"P 或 Q"
• 蕴涵（$\to$）：如果...则...，$P\to Q$ 表示"P 蕴涵 Q"
• 等价（$\leftrightarrow$）：当且仅当，$P\leftrightarrow Q$ 表示"P 和 Q 同真同假"

蕴涵连接词 $P\to Q$ 的语义容易让人困惑。它的真值表定义是：只有当 $P$ 为真且 $Q$ 为假时整个蕴涵式才为假，其余情况都为真。这意味着"假命题蕴涵任何命题"，这并非日常语言中"如果...则..."的含义，而是逻辑学中的一种约定。在工程上，这种约定使得逻辑推理可以被机械化执行，不需要理解命题的实际含义。

真值表与等价推理

真值表是判定命题公式语义的基本工具。对于含有 $n$ 个变量的公式，真值表有 $2^n$ 行，列出所有可能的赋值组合及其对应的公式真值。这种暴力枚举的方式虽然完备，但指数级增长的行数使得它在大规模问题上不可行。 一些重要的逻辑等价式在实际推理中频繁使用。德摩根律 $\mathrm{\neg }(P\wedge Q)\equiv \mathrm{\neg }P\vee \mathrm{\neg }Q$ 和 $\mathrm{\neg }(P\vee Q)\equiv \mathrm{\neg }P\wedge \mathrm{\neg }Q$ 将否定分配到连接词内部，对消解推理至关重要。蕴涵消去 $P\to Q\equiv \mathrm{\neg }P\vee Q$ 将蕴涵转化为析取，大多数自动推理系统在内部都会执行这个转换。逆否命题 $P\to Q\equiv \mathrm{\neg }Q\to \mathrm{\neg }P$ 是一种重要的推理策略，当正向推理困难时可以从反面入手。

一阶谓词逻辑

命题逻辑的表达能力有限，它只能把每个命题看作一个不可分割的整体符号。当需要表达"所有用户都有密码"或者"存在一个管理员在线"这样的陈述时，命题逻辑需要为每种具体情况创建独立的命题变量，根本无法表达量化的语义。一阶谓词逻辑（First-Order Logic）引入了谓词、函数和量词，极大增强了表达能力。

谓词与个体

谓词（Predicate）描述个体（Individual）的性质或关系。Human(socrates) 表示"苏格拉底是人"，Parent(john, mary) 表示"John 是 Mary 的父母"。谓词可以接受一个或多个参数，参数个数称为谓词的元数。一个谓词加上具体参数后就是一个命题，有确定的真值。 函数（Function）从一个个体映射到另一个个体。father(john) 返回 John 的父亲这个个体，age(socrates) 返回苏格拉底的年龄。函数和谓词的区别在于：函数返回一个个体，谓词返回真或假。

量词

量词是一阶逻辑超越命题逻辑的关键机制。全称量词 $\mathrm{\forall }xP(x)$ 表示"对于所有的 $x$，$P(x)$ 都成立"。存在量词 $\mathrm{\exists }xP(x)$ 表示"存在至少一个 $x$ 使得 $P(x)$ 成立"。 量词的嵌套会产生微妙的语义差异。$\mathrm{\forall }x\mathrm{\exists }yLoves(x,y)$ 表示"每个人都至少爱一个人"，而 $\mathrm{\exists }y\mathrm{\forall }xLoves(x,y)$ 表示"存在一个人被所有人爱"。交换量词的顺序改变了整个句子的含义，这在将自然语言翻译为逻辑公式时是最常见的错误来源。 在工程实践中，量词的使用需要特别注意变元的作用域。$\mathrm{\forall }x(P(x)\to Q(x))$ 和 $\mathrm{\forall }xP(x)\to Q(x)$ 是不同的：前者 $x$ 的作用域覆盖整个蕴涵式，后者中 $Q(x)$ 的 $x$ 是自由变量，不受量词约束。

一阶逻辑的语义

一阶逻辑的语义基于解释（Interpretation）的概念。一个解释指定了论域（个体集合）、每个常量符号对应的个体、每个函数符号对应的映射关系、每个谓词符号对应的关系。给定一个解释，可以判定任何公式的真值。有效公式是在所有解释下都为真的公式（类似重言式），可满足公式是存在至少一个解释使其为真的公式。 一阶逻辑的可靠性和完备性定理是元理论的核心成果。可靠性保证：如果公式可以从公理系统中推导出来，那么它在所有满足公理的解释下都为真——推理不会产生错误结论。完备性保证：如果公式在所有满足公理的解释下都为真，那么它可以从公理系统中推导出来——所有正确结论都可以被推导。这两个性质共同确保了逻辑推理系统是值得信赖的。

推理规则

推理规则是从已知前提得出结论的机械步骤，是自动推理的理论基础。

假言推理

假言推理（Modus Ponens）是最基本的推理规则：已知 $P\to Q$ 和 $P$，可以得出 $Q$。这条规则几乎出现在所有推理系统中，从简单的专家系统到复杂的定理证明器。它的直觉含义很简单：如果"P 蕴涵 Q"成立，而且 P 确实成立，那么 Q 也必然成立。 全称实例化是处理量词的基本规则：从 $\mathrm{\forall }xP(x)$ 可以得出 $P(a)$，其中 $a$ 是论域中的任意个体。这条规则将一般性规律应用到具体案例，是前向链推理的起点。类似地，存在实例化从 $\mathrm{\exists }xP(x)$ 得出 $P(c)$，其中 $c$ 是一个新的常量符号（Skolem 常量）。

归结原理

归结原理（Resolution）是 Robinson 在 1965 年提出的单一推理规则，它彻底改变了自动定理证明领域。归结规则如下：从 $(P\vee Q)$ 和 $(\mathrm{\neg }P\vee R)$ 可以得出 $(Q\vee R)$。$P$ 和 $\mathrm{\neg }P$ 是互补文字，它们在归结过程中被消去。 归结原理的强大之处在于：只需要这一条规则，加上反证法策略，就构成了一个完备的推理系统。具体做法是将待证公式的否定转化为子句集，然后反复应用归结规则。如果推导出空子句（矛盾），就证明了原公式成立。

示例：证明 "Socrates 是会死的"
前提：
  1. ∀x (Human(x) → Mortal(x))   /* 所有人都是会死的 */
  2. Human(socrates)               /* 苏格拉底是人 */

转化为子句集：
  1. ¬Human(x) ∨ Mortal(x)
  2. Human(socrates)

归结过程：
  对子句 1（取 x = socrates）和子句 2 进行归结：
  ¬Human(socrates) ∨ Mortal(socrates)
  Human(socrates)
  ─────────────────────
  Mortal(socrates)               /* 结论：苏格拉底会死 */

归结原理在工程实现中面临的主要问题是搜索空间爆炸。即使对于中等复杂度的问题，可能生成的归结式数量也会指数增长。各种启发式策略（如优先对含较少文字的子句进行归结、设置文字数量上限等）在实际系统中被广泛采用。

统一算法

统一（Unification）是归结在一阶逻辑中处理变量的关键机制。两个含有变量的项可以通过统一找到一种变量替换，使得替换后的两个项完全相同。比如 $P(x,a)$ 和 $P(b,y)$ 可以通过替换 $\{x/b,y/a\}$ 统一为 $P(b,a)$。 统一算法需要处理的情况包括：变量与常量的统一、变量与复合项的统一（如 $x$ 和 $f(a)$）、两个复合项的统一（要求函数符和参数个数相同）。出现检查（Occurs Check）防止将变量统一为包含自身的项，比如不能将 $x$ 统一为 $f(x)$，否则会产生无限递归。

推理类型

演绎推理（Deduction）从一般到特殊，前提为真时结论必然为真。经典的三段论"所有人都是会死的，苏格拉底是人，所以苏格拉底会死的"就是演绎推理。演绎推理不产生新知识，只是将前提中隐含的信息显式化。数学证明、程序验证等需要绝对可靠性的场景都依赖演绎推理。 归纳推理（Induction）从特殊到一般，从有限观察中总结普遍规律。观察了 1000 只天鹅都是白色的，归纳出"所有天鹅都是白色的"——第 1001 只黑天鹅就可能推翻这个结论。归纳推理的结论是或然的而非必然的，但它是科学发现和机器学习的基本模式。机器学习本质上就是 一种自动化的归纳过程：从训练数据中归纳出模型，期望模型在未见数据上也能表现良好。 溯因推理（Abduction）从结果反推原因。已知"下雨则地湿"和"地湿"，推测"可能下雨了"。溯因推理的结论不一定正确（也可能有人洒水了），但它是诊断推理的核心方法。医疗诊断、故障排查、刑侦推理都依赖溯因推理——从观察到的症状或现象出发，寻找最合理的解释。 三种推理在 AI 系统中各有其位：演绎推理用于确保结论的可靠性，归纳推理用于从数据中学习，溯因推理用于诊断和解释。理想的 AI 系统应该能灵活运用三种推理模式。

可满足性问题

布尔可满足性问题（Boolean Satisfiability Problem，SAT）是计算复杂性理论的核心问题：给定一个命题逻辑公式，判断是否存在一种变量赋值使得公式为真。SAT 是第一个被证明为 NP 完全的问题（Cook-Levin 定理，1971 年），这意味着如果找到多项式时间的 SAT 算法，所有 NP 问题都可以在多项式时间内解决。 尽管 SAT 在最坏情况下是指数复杂度的，但现代 SAT 求解器（如 MiniSat、Z3）在实际工程问题上表现出了惊人的效率。DPLL 算法通过布尔约束传播（BCP）和纯文字消除快速缩小搜索空间，CDCL（Conflict-Driven Clause Learning）在遇到冲突时学习新的子句避免重复搜索相同的无效路径。 SAT 求解器的工程价值远超学术意义。硬件验证中使用 SAT 求解器检查芯片设计的正确性，软件验证中用其分析程序的可达路径，密码分析中用 SAT 方法破解加密算法，调度和规划问题也可以编码为 SAT 实例求解。Z3 求解器被广泛集成在各类开发工具中，从编译器优化到安全漏洞检测都有它的身影。

从逻辑到 AI

数理逻辑为符号 AI 提供了严格的形式化框架，但"用逻辑就能实现智能"这个假设存在根本性的局限。逻辑要求知识被显式编码为符号和规则，而现实中大量知识是隐性的、模糊的、难以形式化的。命题逻辑表达能力不足，一阶逻辑推理计算代价高昂，更高阶的逻辑甚至不可判定。 尽管如此，数理逻辑的价值并未因深度学习的兴起而减弱。在需要可靠性、可解释性的场景中，逻辑推理仍然是不可替代的工具。程序验证依赖逻辑证明，知识图谱建立在描述逻辑之上，SAT 求解器广泛用于工程验证。理解数理逻辑，不仅是理解符号 AI 的前提，也是理解现代计算理论的基础。