第08章 一阶逻辑

摘要:本章系统介绍一阶逻辑(First-Order Logic, FOL)作为结构化知识表示语言的核心概念。从命题逻辑的表达力不足出发,引入对象、关系、函数、量词等基本构件,详细阐述 FOL 的语法、语义及量词使用规范。通过亲属关系、Peano 公理、集合论等实例展示 FOL 的建模能力,并与命题逻辑在表达力、推理复杂度等方面进行对比。最后探讨 FOL 在知识工程中的实践流程,以及与现代 AI(大语言模型、多模态系统)的关联与启示。

对应 Artificial Intelligence: A Modern Approach, 4th Edition 第 8 章 First-Order Logic


1. 章节概述

本章动机

第 7 章末尾留下了一个明确的痛点:命题逻辑虽然可靠、完备、可判定,但表达力太弱。要说“所有与坑相邻的格子都有微风”,命题逻辑必须为 16 个格子写 16 条句子;若洞穴是 100×100,就要写 10000 条;若格子数未知,则根本无法书写。命题逻辑的世界是一堆互不相关的布尔开关,它看不见“格子”这种对象,也看不见“相邻”这种关系。

核心思想

本章引入 一阶逻辑(First-Order Logic, FOL;也叫 first-order predicate calculus, FOPC),它是人类迄今为止使用最广泛的通用知识表示语言。核心思想:

世界由对象(objects)构成,对象之间存在关系(relations)与函数(functions),我们可以用变量量词对整类对象作断言。

这一步跨越是从因子化表示(factored representation)到结构化表示(structured representation)的质变。

收益与代价

收益

  • 简洁性:一条 ∀x,y …\forall x,y\ \dotsx,y  顶替成千上万条命题句。
  • 通用性:规则与具体对象解耦,知识可迁移到新对象、新规模。
  • 组合性:新对象出现时无须重写规则。

代价

  • 半可判定性:FOL 的蕴涵判定是半可判定的(semi-decidable)——若 KB⊨αKB \models \alphaKBα,算法必定在有限步内确认;若 KB⊭αKB \not\models \alphaKBα,算法可能永不停机(Church–Turing 不可判定性结果)。第 9 章将处理这一现实。

主要内容与学习目标

本章将系统讲解:

  1. 表示语言的再审视:形式语言 vs 自然语言,Sapir–Whorf 假说,为什么需要“组合性”(compositionality)。
  2. FOL 的本体论承诺与认识论承诺
  3. FOL 语法:常量、变量、谓词、函数、项、原子句子、复合句子、量词。
  4. FOL 语义:解释(interpretation)、模型、论域、赋值。
  5. 量词的深层语义∀\forall⇒\Rightarrow 的配对、∃\exists∧\wedge 的配对、嵌套量词、量词对偶。
  6. 等词(equality)与唯一名称假设、唯一量词。
  7. FOL 的工程实践:用 FOL 表示亲属关系、集合、Wumpus World;TELL/ASK 接口;数据库语义。
  8. 知识工程方法论(knowledge engineering process)。

学习目标:掌握 FOL 的基本语法与语义,理解其相对于命题逻辑的表达力提升与计算代价,能够用 FOL 对简单领域进行知识表示,并为后续章节(推理、知识表示、规划等)打下坚实基础。

2. 关键概念与定义

2.1 表示语言的两个维度

任何知识表示语言都要回答两个问题:

承诺类型 含义 命题逻辑 一阶逻辑 时序逻辑 概率论 模糊逻辑
本体论承诺
(ontological commitment)
世界"由什么构成" 事实 事实、对象、关系 事实、对象、关系、时间 事实 有真值度的事实
认识论承诺
(epistemological commitment)
智能体对句子能持有的"信念状态" true / false / unknown true / false / unknown true / false / unknown [0,1][0,1][0,1] 置信度 [0,1][0,1][0,1] 真值度

关键区分

  • 概率论与命题逻辑的本体论承诺相同(都只承认"事实"),差别在认识论——概率允许"70% 相信"。
  • FOL 的本体论承诺更丰富:它承认世界里有离散可辨识的对象
  • 模糊逻辑改变的是本体论:它认为"高"这个属性本身就有程度,而非我们不确定。

2.2 形式语言 vs 自然语言

  • 自然语言不是纯粹的表示语言,它同时承担交流功能,依赖语境(“Look!” 的含义完全取决于情境)。
  • 自然语言有歧义(“Small dogs and cats” 有两种解析)。
  • 形式语言追求无歧义组合性(compositionality):复合句的意义由其组成部分的意义决定。

Sapir–Whorf 假说(语言相对论):语言影响思维。书中以颜色词汇、澳洲原住民语言的绝对方位词(用东南西北而非左右)为例说明语言确实影响认知表现。对 AI 的启示:选择什么表示语言,深刻影响系统能想到什么

2.3 FOL 的世界模型

一个 FOL 模型由三部分构成:

  1. 论域(domain):对象的非空集合 D={d1,d2,… }D = \{d_1, d_2, \dots\}D={d1,d2,}。对象是"世界里的东西":人、格子、数字、颜色、战争、世纪 —— 只要能被指称即可。
  2. 关系(relations):nnn 元关系是 DnD^nDn 的子集。例如 Brother 是有序对的集合 {⟨Richard,John⟩,⟨John,Richard⟩}\{\langle \text{Richard}, \text{John}\rangle, \langle \text{John}, \text{Richard}\rangle\}{⟨Richard,John,John,Richard⟩}。一元关系称为属性(property),如 PersonRound
  3. 函数(functional relations):每个输入元组恰好对应一个输出对象的全函数。例如 LeftLeg(Richard) = 理查德的左腿

⚠️ FOL 要求函数是全函数(total function):论域中每个元组都必须有值。所以 LeftLeg(冠冕) 也必须有值——通常约定为某个"无意义对象"。这是 FOL 的一个技术性代价。

术语解释

  • 元组(tuple):有序对象序列,写作 ⟨d1,…,dn⟩\langle d_1,\dots,d_n\rangled1,,dn
  • 解释(interpretation):把语言中的符号映射到模型中的元素。常量 → 对象,谓词 → 关系,函数符号 → 函数。
  • 若论域有 ∣D∣|D|D 个对象,符号有多种解释方式,则模型数量爆炸增长(甚至无限,因为论域可以任意大)。这解释了为什么 FOL 无法用"枚举模型"做蕴涵判定。

2.4 FOL 语法(完整 BNF)

Sentence        → AtomicSentence | ComplexSentence

AtomicSentence  → Predicate | Predicate(Term, ...) | Term = Term

ComplexSentence → ( Sentence )
                | ¬ Sentence
                | Sentence ∧ Sentence
                | Sentence ∨ Sentence
                | Sentence ⇒ Sentence
                | Sentence ⇔ Sentence
                | Quantifier Variable, ... Sentence

Term            → Function(Term, ...) | Constant | Variable

Quantifier      → ∀ | ∃
Constant        → A | X1 | John | 2 | ...
Variable        → a | x | s | ...
Predicate       → True | False | After | Loves | Raining | ...
Function        → Mother | LeftLeg | Sqrt | ...

算符优先级(高→低):¬, =, ∧, ∨, ⇒, ⇔

符号三类

类型 指称对象 例子
常量符号(constant symbol) 对象 RichardJohn2
谓词符号(predicate symbol) 关系 BrotherOnHeadKing
函数符号(function symbol) 函数 LeftLegMotherSqrt

(term):指称对象的逻辑表达式。

  • 常量是项:John
  • 变量是项:x
  • 函数应用于项仍是项:LeftLeg(John)Mother(Mother(John))

复合项(complex term)的价值:无需为每个对象起名字。相比给理查德的左腿起名 RichardsLeftLeg,写 LeftLeg(Richard) 更简洁且组合性更好

原子句子(atomic sentence):谓词符号 + 项列表,如 Brother(Richard, John)Married(Father(Richard), Mother(John))。原子句子在模型中为真 iff 谓词所指关系确实包含项所指对象构成的元组。

2.5 量词

全称量词 ∀(universal quantification)

∀x P(x)\forall x\ P(x)x P(x)

读作"对所有 xxxP(x)P(x)P(x) 成立"。语义:对论域中每一个对象 ddd,把 xxx 解释为 dddPPP 都为真。

惯用搭配:∀\forall 几乎总与 ⇒\Rightarrow 连用

∀x King(x)⇒Person(x)\forall x\ King(x) \Rightarrow Person(x)x King(x)Person(x)

“所有国王都是人。”

⚠️ 经典错误:用 ∧\wedge 代替 ⇒\Rightarrow

∀x King(x)∧Person(x)\forall x\ King(x) \wedge Person(x)x King(x)Person(x)

这断言"论域中一切东西都是国王并且是人"——包括你的鞋和冠冕。这是初学者最常见的错误。

为什么 ⇒\Rightarrow 正确King(x)⇒Person(x)King(x)\Rightarrow Person(x)King(x)Person(x) 对非国王的 xxx 空真(vacuously true),因此该句只对国王施加约束。

存在量词 ∃(existential quantification)

∃x P(x)\exists x\ P(x)x P(x)

读作"存在某个 xxx 使 P(x)P(x)P(x) 成立"。语义:至少有一个对象使 PPP 为真。

惯用搭配:∃\exists 几乎总与 ∧\wedge 连用

∃x Crown(x)∧OnHead(x,John)\exists x\ Crown(x) \wedge OnHead(x, John)x Crown(x)OnHead(x,John)

“有一顶冠冕在约翰头上。”

⚠️ 经典错误:用 ⇒\Rightarrow 代替 ∧\wedge

∃x Crown(x)⇒OnHead(x,John)\exists x\ Crown(x) \Rightarrow OnHead(x, John)x Crown(x)OnHead(x,John)

这句话几乎必然为真——只要论域中存在任何非冠冕的东西(如太阳),Crown(太阳)Crown(\text{太阳})Crown(太阳) 为假,蕴涵式为真,整个 ∃\exists 就被满足了。这是空洞的真,完全没表达出想说的意思。

记忆口诀

∀\forall⇒\Rightarrow(限定范围再断言);∃\exists∧\wedge(既是又是)。

量词的直观语义(连词/析词展开)

若论域为 {d1,d2,…,dn}\{d_1, d_2, \dots, d_n\}{d1,d2,,dn}

∀x P(x)≡P(d1)∧P(d2)∧⋯∧P(dn)\forall x\ P(x) \quad\equiv\quad P(d_1) \wedge P(d_2)\wedge\cdots\wedge P(d_n)x P(x)P(d1)P(d2)P(dn)

∃x P(x)≡P(d1)∨P(d2)∨⋯∨P(dn)\exists x\ P(x) \quad\equiv\quad P(d_1) \vee P(d_2)\vee\cdots\vee P(d_n)x P(x)P(d1)P(d2)P(dn)

∀\forall无穷合取∃\exists无穷析取。这个视角对理解量词至关重要,也是第 9 章"命题化"(propositionalization)的理论基础。⚠️ 但注意:论域可能无限,所以这只是语义直觉,不是可执行的展开。

嵌套量词(nested quantifiers)
  • 同类量词可交换∀x ∀y≡∀y ∀x\forall x\ \forall y \equiv \forall y\ \forall xx yy x(可简写 ∀x,y\forall x,yx,y);∃x ∃y≡∃y ∃x\exists x\ \exists y \equiv \exists y\ \exists xx yy x
  • 异类量词不可交换

∀x ∃y Loves(x,y)≢∃y ∀x Loves(x,y)\forall x\ \exists y\ Loves(x,y) \quad\not\equiv\quad \exists y\ \forall x\ Loves(x,y)x y Loves(x,y)y x Loves(x,y)

左边:“每个人都爱某个人(各自可以爱不同的人)”
右边:“存在某个人被所有人爱(同一个人)”
右边比左边∃y∀x⊨∀x∃y\exists y\forall x \models \forall x\exists yyxxy,反之不成立。

  • 变量遮蔽(shadowing):∀x [Crown(x)∨(∃x Brother(Richard,x))]\forall x\ [Crown(x) \vee (\exists x\ Brother(Richard, x))]x [Crown(x)(x Brother(Richard,x))] 中内层 xxx 遮蔽外层。应避免这种写法。
  • 约束变量(bound variable)与自由变量(free variable):被量词绑定的是约束变量。没有自由变量的句子称为闭句(closed sentence / 语句 sentence)。
量词对偶(duality)

∀x ¬P≡¬∃x P¬∀x P≡∃x ¬P∀x P≡¬∃x ¬P∃x P≡¬∀x ¬P \begin{aligned} \forall x\ \neg P &\equiv \neg \exists x\ P \\ \neg \forall x\ P &\equiv \exists x\ \neg P \\ \forall x\ P &\equiv \neg \exists x\ \neg P \\ \exists x\ P &\equiv \neg \forall x\ \neg P \end{aligned} x ¬P¬∀x Px Px P¬∃x Px ¬P¬∃x ¬P¬∀x ¬P

理论上只需一个量词即可(另一个用否定定义),但两个都保留更符合直觉。De Morgan 律的量词版本:

命题版 量词版
¬(P∨Q)≡¬P∧¬Q\neg(P\vee Q)\equiv \neg P\wedge\neg Q¬(PQ)¬P¬Q ¬∃x P≡∀x ¬P\neg\exists x\ P \equiv \forall x\ \neg P¬∃x Px ¬P
¬(P∧Q)≡¬P∨¬Q\neg(P\wedge Q)\equiv\neg P\vee\neg Q¬(PQ)¬P¬Q ¬∀x P≡∃x ¬P\neg\forall x\ P\equiv\exists x\ \neg P¬∀x Px ¬P

2.6 等词(Equality)

term1=term2term_1 = term_2term1=term2

当且仅当两个项指称同一个对象时为真。

用途:

  • 断言同一性:Father(John)=HenryFather(John) = HenryFather(John)=Henry
  • 断言差异(配合否定):¬(Richard=John)\neg(Richard = John)¬(Richard=John),常写作 Richard≠JohnRichard \neq JohnRichard=John

表达"恰好两个兄弟"

∃x,y Brother(x,Richard)∧Brother(y,Richard)∧¬(x=y)∧[∀z Brother(z,Richard)⇒(z=x∨z=y)]\exists x,y\ Brother(x,Richard) \wedge Brother(y,Richard) \wedge \neg(x=y) \wedge [\forall z\ Brother(z,Richard) \Rightarrow (z=x \vee z=y)]x,y Brother(x,Richard)Brother(y,Richard)¬(x=y)[z Brother(z,Richard)(z=xz=y)]

⚠️ 若省略 ¬(x=y)\neg(x=y)¬(x=y),则 xxxyyy 可以是同一个人,句子退化为"至少一个兄弟"。

2.7 三个重要假设

假设 含义 后果
唯一名称假设
(Unique-Names Assumption)
不同常量指称不同对象 无需显式写 Richard≠JohnRichard\neq JohnRichard=John;但失去表达"同一对象两个名字"的能力
封闭世界假设
(Closed-World Assumption)
未被断言为真的原子句子为假 数据库语义;使推理可判定,但违反 FOL 的开放世界语义
域闭包
(Domain Closure)
每个模型的对象不多于常量符号所命名者 论域有限且确定

三者合起来称为数据库语义(database semantics),是关系数据库、Prolog、Datalog 采用的语义。它与标准 FOL 的开放世界语义(open-world semantics)形成对比。

如何选择

  • 表示"世界的完整已知描述"(如公司员工表)→ 数据库语义方便。
  • 表示"部分知识 + 通用规律"(如常识推理、Wumpus World)→ 开放世界语义必要。

2.8 唯一量词(Uniqueness Quantifier)

常见简写:

∃! x P(x)≡∃x [P(x)∧∀y (P(y)⇒y=x)]\exists!\, x\ P(x) \quad\equiv\quad \exists x\ \big[ P(x) \wedge \forall y\ (P(y) \Rightarrow y = x) \big]!x P(x)x [P(x)y (P(y)y=x)]

“恰好存在一个 xxx 使 P(x)P(x)P(x) 成立”。展开后依赖等词,所以 ∃!\exists!! 不是 FOL 的原始构造,而是语法糖

相关简写:

  • 唯一性算子 / 摹状词(iota operator):ι x P(x)\iota\, x\ P(x)ιx P(x) 表示"那个满足 PPPxxx"。如 ι x (Brother(x,Richard))\iota\, x\ (Brother(x, Richard))ιx (Brother(x,Richard)) = “理查德的那个兄弟”。同样可归约为 FOL + 等词(罗素的摹状词理论)。

⚠️ 这些简写让公式更易读,但推理引擎通常先展开为标准 FOL。


3. 核心理论与算法

3.1 FOL 的语义:完整定义

模型 MMM = ⟨D,I⟩\langle D, I\rangleD,IDDD 是论域,III 是解释函数:

  • I(常量)∈DI(\text{常量}) \in DI(常量)D
  • I(n-元谓词)⊆DnI(n\text{-元谓词}) \subseteq D^nI(n-元谓词)Dn
  • I(n-元函数):Dn→DI(n\text{-元函数}): D^n \to DI(n-元函数):DnD

项的指称(denotation)递归定义,记 ⟦t⟧M,σ\llbracket t \rrbracket_{M,\sigma}[[t]]M,σσ\sigmaσ 为变量赋值):

  • ⟦c⟧=I(c)\llbracket c \rrbracket = I(c)[[c]]=I(c)
  • ⟦x⟧=σ(x)\llbracket x \rrbracket = \sigma(x)[[x]]=σ(x)
  • ⟦f(t1,…,tn)⟧=I(f)(⟦t1⟧,…,⟦tn⟧)\llbracket f(t_1,\dots,t_n)\rrbracket = I(f)(\llbracket t_1\rrbracket,\dots,\llbracket t_n\rrbracket)[[f(t1,,tn)]]=I(f)([[t1]],,[[tn]])

句子的真值

  • M,σ⊨P(t1,…,tn)M,\sigma \models P(t_1,\dots,t_n)M,σP(t1,,tn) iff ⟨⟦t1⟧,…,⟦tn⟧⟩∈I(P)\langle \llbracket t_1\rrbracket,\dots,\llbracket t_n\rrbracket\rangle \in I(P)[[t1]],,[[tn]]I(P)
  • M,σ⊨t1=t2M,\sigma \models t_1 = t_2M,σt1=t2 iff ⟦t1⟧=⟦t2⟧\llbracket t_1\rrbracket = \llbracket t_2\rrbracket[[t1]]=[[t2]]
  • 连接词按命题逻辑真值表
  • M,σ⊨∀x αM,\sigma \models \forall x\ \alphaM,σx α iff 对每个 d∈Dd\in DdDM,σ[x↦d]⊨αM, \sigma[x\mapsto d] \models \alphaM,σ[xd]α
  • M,σ⊨∃x αM,\sigma \models \exists x\ \alphaM,σx α iff 存在某个 d∈Dd\in DdDM,σ[x↦d]⊨αM, \sigma[x\mapsto d] \models \alphaM,σ[xd]α

蕴涵定义与第 7 章相同KB⊨αKB \models \alphaKBα iff 每个满足 KBKBKB 的模型都满足 α\alphaα。差别在于模型的数量与结构远为复杂(论域大小无界,解释方式无穷多)。

3.2 为什么 FOL 蕴涵只是半可判定的

  • Gödel 完备性定理(1930):存在可靠且完备的证明系统,若 KB⊨αKB\models\alphaKBα 则存在有限长证明。
  • Church–Turing 不可判定性(1936):FOL 的有效性判定问题是不可判定的

两者结合:

FOL 蕴涵是半可判定(semi-decidable / recursively enumerable)的:可以设计算法在 KB⊨αKB\models\alphaKBα一定终止并答"是",但在 KB⊭αKB\not\models\alphaKBα 时可能永远运行下去

对比表

逻辑 蕴涵判定 复杂度
命题逻辑 可判定 co-NP-完全
一阶逻辑 半可判定 不可判定
FOL 无函数符号、有限常量(Datalog) 可判定 EXPTIME(数据复杂度多项式)
描述逻辑(如 ALC\mathcal{ALC}ALC 可判定 PSPACE / EXPTIME

这就是为什么实用系统常常故意限制表达力(Datalog、描述逻辑、OWL),用表达力换可判定性与效率——这是知识表示领域的核心权衡(第 10 章会详细讨论)。

3.3 与命题逻辑的严格对比

维度 命题逻辑 一阶逻辑
基本单元 命题符号(不透明) 对象、关系、函数
变量
量词 ∀\forall∃\exists
表达"所有 X 都 Y" 必须逐个枚举,O(n)O(n)O(n)O(n2)O(n^2)O(n2) 一条句子
未知数量的对象 无法表示 自然表示
模型数量 2n2^n2n(有限) 无限(论域大小无界)
蕴涵判定 可判定,co-NP-完全 半可判定
推理算法 真值表、DPLL、归结 unification + lifted resolution(第 9 章)
知识可复用性 差(规则与实例绑定) 好(规则与实例解耦)

Wumpus World 的对比实例

命题逻辑(需要 16 条,4×44\times44×4 网格):

B₁,₁ ⟺ (P₁,₂ ∨ P₂,₁)
B₁,₂ ⟺ (P₁,₁ ∨ P₁,₃ ∨ P₂,₂)
B₂,₁ ⟺ (P₁,₁ ∨ P₂,₂ ∨ P₃,₁)
...共 16 条...

一阶逻辑(一条):

∀s  Breezy(s)⇔∃r  Adjacent(r,s)∧Pit(r)\forall s\ \ Breezy(s) \Leftrightarrow \exists r\ \ Adjacent(r, s) \wedge Pit(r)s  Breezy(s)r  Adjacent(r,s)Pit(r)

不仅短,而且与网格大小无关:100×100 的洞穴用同一条句子。这就是结构化表示的力量。

3.4 用 FOL 表示知识:亲属关系领域

词汇设计(vocabulary / signature):

  • 一元谓词:Male(x)Male(x)Male(x)Female(x)Female(x)Female(x)
  • 二元谓词:Parent(x,y)Parent(x,y)Parent(x,y)Sibling(x,y)Sibling(x,y)Sibling(x,y)ChildChildChildSpouseSpouseSpouseBrotherBrotherBrotherSisterSisterSisterDaughterDaughterDaughterSonSonSonGrandparentGrandparentGrandparentGrandchildGrandchildGrandchildUncleUncleUncleAuntAuntAunt
  • 函数:Mother(x)Mother(x)Mother(x)Father(x)Father(x)Father(x)(因为每人恰有一个生母/生父)

公理(axioms):

∀m,c  Mother(c)=m⇔Female(m)∧Parent(m,c)∀w,h  Husband(h,w)⇔Male(h)∧Spouse(h,w)∀x  Male(x)⇔¬Female(x)∀p,c  Parent(p,c)⇔Child(c,p)∀g,c  Grandparent(g,c)⇔∃p  Parent(g,p)∧Parent(p,c)∀x,y  Sibling(x,y)⇔x≠y∧∃p  Parent(p,x)∧Parent(p,y) \begin{aligned} &\forall m,c\ \ Mother(c) = m \Leftrightarrow Female(m) \wedge Parent(m,c) \\ &\forall w,h\ \ Husband(h,w) \Leftrightarrow Male(h) \wedge Spouse(h,w) \\ &\forall x\ \ Male(x) \Leftrightarrow \neg Female(x) \\ &\forall p,c\ \ Parent(p,c) \Leftrightarrow Child(c,p) \\ &\forall g,c\ \ Grandparent(g,c) \Leftrightarrow \exists p\ \ Parent(g,p)\wedge Parent(p,c) \\ &\forall x,y\ \ Sibling(x,y) \Leftrightarrow x\neq y \wedge \exists p\ \ Parent(p,x)\wedge Parent(p,y) \end{aligned} m,c  Mother(c)=mFemale(m)Parent(m,c)w,h  Husband(h,w)Male(h)Spouse(h,w)x  Male(x)¬Female(x)p,c  Parent(p,c)Child(c,p)g,c  Grandparent(g,c)p  Parent(g,p)Parent(p,c)x,y  Sibling(x,y)x=yp  Parent(p,x)Parent(p,y)

术语区分

  • 定义(definition):形如 ⇔\Leftrightarrow 的句子,用已有概念完全刻画新概念。上面大多数是定义。
  • 定理(theorem):可由其他公理推出的句子,如 ∀x,y Sibling(x,y)⇔Sibling(y,x)\forall x,y\ Sibling(x,y)\Leftrightarrow Sibling(y,x)x,y Sibling(x,y)Sibling(y,x)。加入 KB 不增加信息,但可能加速推理
  • 独立公理(independent axiom):不可由其他句子推出,如 ∀x Male(x)⇔¬Female(x)\forall x\ Male(x)\Leftrightarrow\neg Female(x)x Male(x)¬Female(x)

⚠️ 并非所有概念都能给出完整定义。Person(x)Person(x)Person(x) 就很难用充要条件定义——这是自然类(natural kind)问题,第 10 章会展开。对此只能给部分刻画(partial specification),用 ⇒\Rightarrow 而非 ⇔\Leftrightarrow

代码示例:用 Python sympy 实现亲属关系推理

下面是一个使用 Python 的 sympy 库来形式化和查询亲属关系公理的简单示例。sympy 是一个符号计算库,可以处理逻辑表达式和推理。

from sympy import symbols, ForAll, Exists, Implies, And, Or, Not, Eq, Function, Predicate
from sympy.logic.inference import satisfiable

# 定义个体常量
john, mary, richard, alice = symbols('john mary richard alice')

# 定义谓词
Male = Predicate('Male')
Female = Predicate('Female')
Parent = Predicate('Parent', arity=2)
Sibling = Predicate('Sibling', arity=2)
Grandparent = Predicate('Grandparent', arity=2)

# 定义变量
x, y, z, p, c, g = symbols('x y z p c g')

# 定义公理
axioms = [
    # 公理1: 男性与女性互斥
    ForAll(x, Eq(Male(x), Not(Female(x)))),
    
    # 公理2: 父母关系的对称性
    ForAll([p, c], Eq(Parent(p, c), Parent(p, c))),  # 自反性
    ForAll([p, c], Implies(Parent(p, c), Parent(p, c))),  # 实际使用中需要更复杂的对称关系
    
    # 公理3: 祖父母定义
    ForAll([g, c], Eq(Grandparent(g, c), 
                     Exists(p, And(Parent(g, p), Parent(p, c))))),
    
    # 公理4: 兄弟姐妹定义(共享父母且不是同一个人)
    ForAll([x, y], Eq(Sibling(x, y), 
                      And(Not(Eq(x, y)), 
                          Exists(p, And(Parent(p, x), Parent(p, y)))))),
    
    # 公理5: 兄弟姐妹的对称性
    ForAll([x, y], Implies(Sibling(x, y), Sibling(y, x))),
]

# 添加具体事实
facts = [
    Male(john),
    Female(mary),
    Parent(john, richard),
    Parent(mary, richard),
    Parent(richard, alice),
    Not(Eq(john, mary)),  # 约翰和玛丽不是同一个人
]

# 组合知识和事实
knowledge_base = axioms + facts

print("=== 知识库中的公理 ===")
for i, axiom in enumerate(axioms, 1):
    print(f"{i}. {axiom}")

print("\n=== 具体事实 ===")
for i, fact in enumerate(facts, 1):
    print(f"{i}. {fact}")

# 查询示例
print("\n=== 查询示例 ===")

# 查询1: 理查德是男性吗?
query1 = Male(richard)
print(f"1. 理查德是男性吗?")
print(f"   查询: {query1}")
# 这个查询无法直接从现有知识推导,需要更多公理

# 查询2: 爱丽丝的祖父母是谁?
query2 = Exists(g, Grandparent(g, alice))
print(f"\n2. 爱丽丝有祖父母吗?")
print(f"   查询: {query2}")

# 手动推理展示
print(f"\n   推理过程:")
print(f"   - 已知: Parent(richard, alice) [理查德是爱丽丝的父母]")
print(f"   - 已知: Parent(john, richard) [约翰是理查德的父母]")
print(f"   - 根据祖父母定义: Grandparent(g, alice) ⇔ ∃p (Parent(g, p) ∧ Parent(p, alice))")
print(f"   - 令 p = richard, g = john:")
print(f"     Parent(john, richard) ∧ Parent(richard, alice) 为真")
print(f"   - 因此: Grandparent(john, alice) 为真")
print(f"   - 结论: 约翰是爱丽丝的祖父母")

# 查询3: 约翰和玛丽是兄弟姐妹吗?
query3 = Sibling(john, mary)
print(f"\n3. 约翰和玛丽是兄弟姐妹吗?")
print(f"   查询: {query3}")
print(f"   需要检查是否存在 p 使得 Parent(p, john) 且 Parent(p, mary)")
print(f"   当前知识库中没有这样的 p,所以答案为假")

# 使用 satisfiable 检查一致性
print("\n=== 知识库一致性检查 ===")
consistency_check = And(*knowledge_base)
result = satisfiable(consistency_check, all_models=False)
if result:
    print("知识库是一致的(至少有一个模型满足所有公理和事实)")
else:
    print("知识库不一致!存在矛盾")

# 添加更多事实进行扩展推理
print("\n=== 扩展推理 ===")
additional_facts = [
    Male(richard),
    Female(alice),
]

extended_kb = knowledge_base + additional_facts

# 检查新知识库的一致性
extended_consistency = And(*extended_kb)
if satisfiable(extended_consistency, all_models=False):
    print("扩展后的知识库仍然一致")
    
    # 现在可以推导更多关系
    print("\n可以推导的结论:")
    print("1. 从 Male(john) 和 ∀x (Male(x) ⇔ ¬Female(x)) 可推出 ¬Female(john)")
    print("2. 从 Parent(john, richard) 和 Parent(richard, alice)")
    print("   根据祖父母定义,可推出 Grandparent(john, alice)")
    print("3. 从 Parent(mary, richard) 和 Parent(richard, alice)")
    print("   可推出 Grandparent(mary, alice)")
else:
    print("扩展后的知识库存在矛盾")

查询结果说明

  1. 祖父母查询:通过公理 Grandparent(g, c) ⇔ ∃p (Parent(g, p) ∧ Parent(p, c)) 和事实 Parent(john, richard)Parent(richard, alice),我们可以推导出 Grandparent(john, alice)。这展示了 FOL 如何通过通用规则结合具体事实进行推理。

  2. 兄弟姐妹查询:查询 Sibling(john, mary) 在当前知识库中为假,因为没有公理表明约翰和玛丽共享父母。要使其为真,需要添加如 Parent(parent1, john)Parent(parent1, mary) 的事实。

  3. 一致性检查:使用 satisfiable() 函数验证知识库是否包含矛盾。这是实际推理系统中的重要步骤,确保添加新知识不会破坏现有知识库。

  4. 扩展推理:添加更多事实后,系统可以推导出更多关系,如 Grandparent(mary, alice)

技术要点

  • sympy 的 Predicate 和量词(ForAllExists)可以很好地表示 FOL 公理
  • satisfiable() 函数用于检查知识库的一致性
  • 实际应用中,需要更完整的推理引擎(如 prover9、Vampire 等)进行自动定理证明
  • 这个示例主要展示形式化表示,完整的自动推理需要更复杂的实现

通过这个示例,我们可以看到如何将 FOL 公理转化为可执行的代码,并进行基本的逻辑查询。在实际的知识工程中,这种形式化是确保推理正确性的基础。

3.5 用 FOL 表示数:Peano 公理

展示 FOL 如何从极少的原语构建整个数学分支。

原语:常量 000,函数 SSS(后继)。

NatNum(0)∀n  NatNum(n)⇒NatNum(S(n))∀n  0≠S(n)0 不是任何数的后继∀m,n  m≠n⇒S(m)≠S(n)S 是单射 \begin{aligned} &NatNum(0) \\ &\forall n\ \ NatNum(n) \Rightarrow NatNum(S(n)) \\ &\forall n\ \ 0 \neq S(n) && \text{0 不是任何数的后继}\\ &\forall m,n\ \ m\neq n \Rightarrow S(m)\neq S(n) && \text{S 是单射} \end{aligned} NatNum(0)n  NatNum(n)NatNum(S(n))n  0=S(n)m,n  m=nS(m)=S(n)不是任何数的后继是单射

加法定义(递归):

∀m  NatNum(m)⇒+(0,m)=m∀m,n  NatNum(m)∧NatNum(n)⇒+(S(m),n)=S(+(m,n)) \begin{aligned} &\forall m\ \ NatNum(m) \Rightarrow +(0,m) = m \\ &\forall m,n\ \ NatNum(m)\wedge NatNum(n) \Rightarrow +(S(m), n) = S(+(m,n)) \end{aligned} m  NatNum(m)+(0,m)=mm,n  NatNum(m)NatNum(n)+(S(m),n)=S(+(m,n))

注意 +++函数符号,可用中缀记法(syntactic sugar)m+nm+nm+nS(S(0))+S(S(S(0)))S(S(0))+S(S(S(0)))S(S(0))+S(S(S(0))) 就是 2+32+32+3

教学价值:说明 FOL 的递归定义能力,以及"用少量公理刻画无限论域"的方法。这与第 10 章的本体工程一脉相承。

3.6 用 FOL 表示集合

原语:常量 { }\{\,\}{}(空集),一元谓词 SetSetSet,二元谓词 ∈\in⊆\subseteq,二元函数 ∩\cap∪\cupAdd(x,s)Add(x,s)Add(x,s)

∀s  Set(s)⇔(s={ })∨(∃x,s2  Set(s2)∧s=Add(x,s2))¬∃x,s  Add(x,s)={ }加元素永不得空集∀x,s  x∈s⇔s=Add(x,s)幂等:加已有元素不变∀x,s  x∈s⇔∃y,s2 (s=Add(y,s2)∧(x=y∨x∈s2))∀s1,s2  s1⊆s2⇔∀x (x∈s1⇒x∈s2)∀s1,s2  (s1=s2)⇔(s1⊆s2∧s2⊆s1)∀x,s1,s2  x∈(s1∩s2)⇔(x∈s1∧x∈s2)∀x,s1,s2  x∈(s1∪s2)⇔(x∈s1∨x∈s2) \begin{aligned} &\forall s\ \ Set(s) \Leftrightarrow (s=\{\,\}) \vee (\exists x, s_2\ \ Set(s_2) \wedge s = Add(x,s_2)) \\ &\neg\exists x,s\ \ Add(x,s) = \{\,\} && \text{加元素永不得空集}\\ &\forall x,s\ \ x\in s \Leftrightarrow s = Add(x,s) && \text{幂等:加已有元素不变}\\ &\forall x,s\ \ x\in s \Leftrightarrow \exists y,s_2\ (s = Add(y,s_2) \wedge (x=y \vee x\in s_2)) \\ &\forall s_1,s_2\ \ s_1\subseteq s_2 \Leftrightarrow \forall x\ (x\in s_1 \Rightarrow x\in s_2) \\ &\forall s_1,s_2\ \ (s_1 = s_2) \Leftrightarrow (s_1\subseteq s_2 \wedge s_2 \subseteq s_1) \\ &\forall x,s_1,s_2\ \ x\in(s_1\cap s_2) \Leftrightarrow (x\in s_1 \wedge x\in s_2) \\ &\forall x,s_1,s_2\ \ x\in(s_1\cup s_2) \Leftrightarrow (x\in s_1 \vee x\in s_2) \end{aligned} s  Set(s)(s={})(x,s2  Set(s2)s=Add(x,s2))¬∃x,s  Add(x,s)={}x,s  xss=Add(x,s)x,s  xsy,s2 (s=Add(y,s2)(x=yxs2))s1,s2  s1s2x (xs1xs2)s1,s2  (s1=s2)(s1s2s2s1)x,s1,s2  x(s1s2)(xs1xs2)x,s1,s2  x(s1s2)(xs1xs2)加元素永不得空集幂等:加已有元素不变

列表同理,用 NilNilNilConsConsConsFindFindFindAppendAppendAppend 等,是 Lisp/Prolog 数据结构的逻辑刻画。

3.7 FOL 中的 Wumpus World

感知的表示

感知是带时间戳的语句:

Percept([Stench,Breeze,Glitter,None,None],5)Percept([Stench, Breeze, Glitter, None, None], 5)Percept([Stench,Breeze,Glitter,None,None],5)

即感知向量 + 时间步。动作用项表示,查询用量词:

ASK(KB, ∃a  BestAction(a,5))\text{ASK}(KB,\ \exists a\ \ BestAction(a, 5))ASK(KB, a  BestAction(a,5))

返回替换/绑定列表(substitution / binding list),如 {a/Grab}\{a/Grab\}{a/Grab}。这是 FOL 的 ASK 与命题逻辑 ASK 的关键差别:不只返回 true/false,还返回满足查询的对象

简单反射规则

∀t,s,g,w,c  Percept([s,Breeze,g,w,c],t)⇒Breeze(t)∀t,s,b,w,c  Percept([s,b,Glitter,w,c],t)⇒Glitter(t)∀t  Glitter(t)⇒BestAction(Grab,t) \begin{aligned} &\forall t,s,g,w,c\ \ Percept([s,Breeze,g,w,c],t) \Rightarrow Breeze(t) \\ &\forall t,s,b,w,c\ \ Percept([s,b,Glitter,w,c],t) \Rightarrow Glitter(t) \\ &\forall t\ \ Glitter(t) \Rightarrow BestAction(Grab, t) \end{aligned} t,s,g,w,c  Percept([s,Breeze,g,w,c],t)Breeze(t)t,s,b,w,c  Percept([s,b,Glitter,w,c],t)Glitter(t)t  Glitter(t)BestAction(Grab,t)

环境公理

∀x,y,a,b  Adjacent([x,y],[a,b])⇔(x=a∧(y=b−1∨y=b+1)) ∨ (y=b∧(x=a−1∨x=a+1))∀s,t  At(Agent,s,t)∧Breeze(t)⇒Breezy(s)∀s  Breezy(s)⇒∃r  Adjacent(r,s)∧Pit(r)∀s  ¬Breezy(s)⇒∀r  Adjacent(r,s)⇒¬Pit(r) \begin{aligned} &\forall x,y,a,b\ \ Adjacent([x,y],[a,b]) \Leftrightarrow \\ &\qquad (x=a \wedge (y=b-1 \vee y=b+1)) \ \vee\ (y=b \wedge (x=a-1\vee x=a+1)) \\[4pt] &\forall s,t\ \ At(Agent,s,t)\wedge Breeze(t) \Rightarrow Breezy(s) \\[4pt] &\forall s\ \ Breezy(s) \Rightarrow \exists r\ \ Adjacent(r,s)\wedge Pit(r) \\[4pt] &\forall s\ \ \neg Breezy(s) \Rightarrow \forall r\ \ Adjacent(r,s)\Rightarrow \neg Pit(r) \end{aligned} x,y,a,b  Adjacent([x,y],[a,b])(x=a(y=b1y=b+1))  (y=b(x=a1x=a+1))s,t  At(Agent,s,t)Breeze(t)Breezy(s)s  Breezy(s)r  Adjacent(r,s)Pit(r)s  ¬Breezy(s)r  Adjacent(r,s)¬Pit(r)

后两条合起来即 ∀s Breezy(s)⇔∃r Adjacent(r,s)∧Pit(r)\forall s\ Breezy(s)\Leftrightarrow\exists r\ Adjacent(r,s)\wedge Pit(r)s Breezy(s)r Adjacent(r,s)Pit(r)一条顶替命题逻辑的 16 条

一个重要的表示细节:对象的同一性

∀x,s,t  At(x,s,t)∧At(x,s2,t)⇒s=s2\forall x,s,t\ \ At(x,s,t) \wedge At(x,s_2,t) \Rightarrow s = s_2x,s,t  At(x,s,t)At(x,s2,t)s=s2

"一个对象在同一时刻只能在一个位置。"这类公理化常识是知识工程的日常工作,也说明为什么 KB 构建困难:太多"显而易见"的事需要显式写出。

3.8 知识工程流程(Knowledge Engineering Process)

书中给出的七步方法论:

1. 确定任务(Identify the questions)
   明确 KB 需要支持哪些查询、什么样的事实可用。

2. 汇集相关知识(Knowledge acquisition)
   知识工程师与领域专家交流,理解领域运作机制。
   注意:此阶段是非形式化的。

3. 确定词汇:谓词、函数、常量(Decide on a vocabulary)
   把领域概念翻译成逻辑符号。这一步称为
   本体(ontology)设计,决定"世界由什么构成"。
   这是最关键也最难的一步。

4. 编码领域通用知识(Encode general knowledge)
   写公理。此过程常暴露第 3 步的词汇缺陷 → 迭代回第 3 步。

5. 编码具体问题实例(Encode the specific problem instance)
   把待解问题的具体事实 TELL 给 KB。

6. 提交查询,获取答案(Pose queries)
   让推理过程工作,这是"收获"阶段。

7. 调试与验证知识库(Debug and evaluate)
   检查答案。错误答案通常源于:
   - 缺失公理(KB 太弱,推不出应有结论)
   - 过强公理(推出错误结论,如把 ⇒ 写成 ⟺)
   - 词汇设计不当

⚠️ 常见错误诊断

  • 推不出结论 → 缺公理,或量词/连接词搭配错。
  • 推出荒谬结论 → 公理过强,或论域中存在未预料的对象。
  • 推理不终止 → 存在可产生无限项的函数符号,或递归定义无基准情形。

书中的电子电路示例(一位加法器)展示了这一流程的完整实践:定义 SignalSignalSignalConnectedConnectedConnectedTypeTypeTypeInInInOutOutOut 等词汇,编码门的行为公理,然后查询"什么输入组合使输出为 ⟨1,0⟩"。这展示了 FOL 作为声明式规约语言的价值——同一个 KB 既能做仿真(给输入求输出)也能做综合(给输出求输入),而过程式程序做不到。


3.9 实战案例:图书馆借阅系统

让我们通过一个简化的图书馆借阅系统,完整走一遍 §3.8 的知识工程流程。

1. 确定任务
  • 查询:会员 Alice 还能借几本书?书 B123 是否已逾期?会员 Bob 能否借阅书 B456
  • 可用事实:会员信息、图书信息、借阅记录、逾期状态。
2. 汇集相关知识
  • 每个会员有唯一 ID,最多可借 5 本书。
  • 每本书有唯一 ISBN,可被借出或留在馆内。
  • 借阅记录包含会员、书、借出日期、应还日期。
  • 若当前日期超过应还日期,该书为逾期状态,该会员不能再借新书。
3. 确定词汇(本体设计)
  • 常量Alice, Bob, B123, B456, 2025-03-20(当前日期)
  • 一元谓词Member(m), Book(b)
  • 二元谓词Borrows(m, b, borrowDate, dueDate)(四元关系,具体化处理见下)
  • 三元谓词Overdue(b, m)(书 b 被会员 m 借阅且已逾期)
  • 函数DueDate(b, m)(返回应还日期),CurrentDate()(返回当前日期)

具体化技巧:为避免四元谓词,我们将借阅事件具体化为对象:

  • 增加一元谓词:BorrowEvent(e)
  • 增加二元谓词:Agent(e, m)(借阅者),Object(e, b)(被借书),StartTime(e, borrowDate)EndTime(e, dueDate)
4. 编码领域通用知识(公理)

类型公理

∀m (Member(m) → Person(m))
∀b (Book(b) → Item(b))
∀e (BorrowEvent(e) → Event(e))

借阅关系定义

∀e,m,b,d1,d2 (BorrowEvent(e) ∧ Agent(e,m) ∧ Object(e,b) ∧ StartTime(e,d1) ∧ EndTime(e,d2))
    → (Member(m) ∧ Book(b) ∧ Borrows(m,b,d1,d2))

逾期定义

∀b,m (Overdue(b,m) ↔ 
    ∃e,d1,d2 (BorrowEvent(e) ∧ Agent(e,m) ∧ Object(e,b) ∧ 
              StartTime(e,d1) ∧ EndTime(e,d2) ∧ 
              CurrentDate() > d2))

业务规则

// 每个会员最多借 5 本书
∀m (Member(m) → 
    ∃≤5 b (∃e,d1,d2 (BorrowEvent(e) ∧ Agent(e,m) ∧ Object(e,b) ∧ 
                     StartTime(e,d1) ∧ EndTime(e,d2) ∧ ¬Overdue(b,m))))

// 逾期书不可再借(会员有逾期书则不能借新书)
∀m,b1,b2,d1,d2 (Overdue(b1,m) ∧ Book(b2) ∧ 
                ¬∃e (BorrowEvent(e) ∧ Agent(e,m) ∧ Object(e,b2)))
    → ¬CanBorrow(m,b2)

// 等价表达:会员可借书的条件是没有逾期书且未达上限
∀m,b (CanBorrow(m,b) ↔ 
      Member(m) ∧ Book(b) ∧ 
      ¬∃b1 (Overdue(b1,m)) ∧ 
      CountBorrowed(m) < 5)

辅助函数/谓词定义(需在 FOL 中展开):

// 计算会员已借书数量(非逾期)
∀m,n (CountBorrowed(m)=n ↔ 
      ∃{b1,...,bn} (∧_i Book(bi) ∧ ∧_i≠j bi≠bj ∧ 
                    ∧_i ∃e,d1,d2 (BorrowEvent(e) ∧ Agent(e,m) ∧ Object(e,bi) ∧ 
                                  StartTime(e,d1) ∧ EndTime(e,d2) ∧ ¬Overdue(bi,m)) ∧
                    ∀b (Book(b) ∧ ∃e,d1,d2 (BorrowEvent(e) ∧ Agent(e,m) ∧ Object(e,b) ∧ 
                                           StartTime(e,d1) ∧ EndTime(e,d2) ∧ ¬Overdue(b,m))
                         → ∨_i b=bi)))
5. 编码具体问题实例
// 会员与图书
Member(Alice)
Member(Bob)
Book(B123)
Book(B456)
Book(B789)

// 当前日期
CurrentDate() = 2025-03-20

// 借阅事件
BorrowEvent(E1)
Agent(E1, Alice)
Object(E1, B123)
StartTime(E1, 2025-03-01)
EndTime(E1, 2025-03-15)  // 已逾期

BorrowEvent(E2)
Agent(E2, Alice)
Object(E2, B456)
StartTime(E2, 2025-03-10)
EndTime(E2, 2025-03-25)  // 未逾期

BorrowEvent(E3)
Agent(E3, Bob)
Object(E3, B789)
StartTime(E3, 2025-03-05)
EndTime(E3, 2025-03-19)  // 已逾期
6. 提交查询示例

查询 1Alice 还能借几本书?

ASK(KB, ∃n (RemainingQuota(Alice, n)))

需推导:

  • Overdue(B123, Alice) 为真(因为 2025-03-20 > 2025-03-15)
  • CountBorrowed(Alice) = 1(只有 B456 未逾期)
  • RemainingQuota(Alice, n) ↔ Member(Alice) ∧ n = 5 - CountBorrowed(Alice) ∧ ¬∃b Overdue(b,Alice)
  • 但由于存在逾期书 B123,¬∃b Overdue(b,Alice) 为假,所以 RemainingQuota(Alice, 0)?实际业务中,有逾期书时 quota 应为 0。

查询 2:书 B123 是否已逾期?

ASK(KB, Overdue(B123, Alice))

直接匹配 Overdue 定义:CurrentDate()=2025-03-20 > EndTime(E1)=2025-03-15,答案为真。

查询 3Bob 能否借阅书 B456

ASK(KB, CanBorrow(Bob, B456))

推导:

  • Overdue(B789, Bob) 为真(2025-03-20 > 2025-03-19)
  • CanBorrow(m,b) 要求 ¬∃b1 Overdue(b1,m),该条件为假
  • 因此 CanBorrow(Bob, B456) 为假
7. 调试与验证

可能发现的缺失公理

  • 应还日期计算规则(如借期 14 天):∀e,m,b,d1 (BorrowEvent(e) ∧ Agent(e,m) ∧ Object(e,b) ∧ StartTime(e,d1) → EndTime(e,d1+14))
  • 同一本书不能被两人同时借阅:∀e1,e2,b (BorrowEvent(e1) ∧ BorrowEvent(e2) ∧ Object(e1,b) ∧ Object(e2,b) ∧ StartTime(e1) ≤ CurrentDate() ∧ EndTime(e1) ≥ CurrentDate() → e1=e2)

词汇设计反思

  • 最初的四元谓词 Borrows(m,b,borrowDate,dueDate) 改为具体化的事件对象,更易扩展(可添加 Renewed(e1,e2)Fine(e,amount) 等)。
  • CurrentDate() 作为零元函数,在真实系统中需随时间变化,这引向情境演算(第 12 章)或时序逻辑的需求。

这个案例展示了如何将业务规则精确翻译为 FOL 公理,也暴露了 FOL 在表达计数(“最多 5 本”)、算术(日期比较)上的繁琐性——这正是实际系统常采用数据库语义(直接 SQL 查询)或混合系统(FOL 规则 + 外部算术函数)的原因。

4. 关键图示/表格说明

4.1 模型的图示(对应原书 Figure 8.2)

书中给出一个含 5 个对象的模型:

对象:Richard the Lionheart(理查德)
      King John(约翰王)
      Richard 的左腿
      John 的左腿
      一顶冠冕

一元关系(属性):
      person = {Richard, John}
      king   = {John}
      crown  = {那顶冠冕}

二元关系:
      brother = {⟨Richard,John⟩, ⟨John,Richard⟩}
      onhead  = {⟨冠冕, John⟩}

一元函数:
      leftleg: Richard ↦ Richard的左腿
               John    ↦ John的左腿

读图要点

  1. 关系是元组的集合,函数是输入到唯一输出的映射
  2. brother 包含两个有序对,体现对称性——但这是模型的性质,不是逻辑强制的;若要保证对称,须写公理 ∀x,y Brother(x,y)⇔Brother(y,x)\forall x,y\ Brother(x,y)\Leftrightarrow Brother(y,x)x,y Brother(x,y)Brother(y,x)
  3. 函数必须是全函数:图中 leftleg 只对两个人定义,严格说需要补上"冠冕的左腿"这类怪异条目。这是 FOL 的技术性妥协。
  4. 符号与对象的分离:常量 Richard符号,理查德本人是对象。同一对象可有多个名字(除非采用唯一名称假设)。

4.2 量词误用对照表(最重要的复习表)

想表达 ✓ 正确写法 ✗ 常见错误 错误后果
所有国王都是人 ∀x King(x)⇒Person(x)\forall x\ King(x)\Rightarrow Person(x)x King(x)Person(x) ∀x King(x)∧Person(x)\forall x\ King(x)\wedge Person(x)x King(x)Person(x) 断言"万物皆国王且皆人"
存在冠冕在约翰头上 ∃x Crown(x)∧OnHead(x,John)\exists x\ Crown(x)\wedge OnHead(x,John)x Crown(x)OnHead(x,John) ∃x Crown(x)⇒OnHead(x,John)\exists x\ Crown(x)\Rightarrow OnHead(x,John)x Crown(x)OnHead(x,John) 只要有非冠冕物体存在就空洞为真
每人都爱某人 ∀x ∃y Loves(x,y)\forall x\ \exists y\ Loves(x,y)x y Loves(x,y) ∃y ∀x Loves(x,y)\exists y\ \forall x\ Loves(x,y)y x Loves(x,y) 变成"有人被所有人爱"(更强)
理查德恰有两个兄弟 ∃x,y B(x,R)∧B(y,R)∧x≠y∧∀z(B(z,R)⇒z=x∨z=y)\exists x,y\ B(x,R)\wedge B(y,R)\wedge x\neq y\wedge \forall z(B(z,R)\Rightarrow z=x\vee z=y)x,y B(x,R)B(y,R)x=yz(B(z,R)z=xz=y) 省略 x≠yx\neq yx=y 退化为"至少一个兄弟"
没有国王是坏人 ∀x King(x)⇒¬Evil(x)\forall x\ King(x)\Rightarrow\neg Evil(x)x King(x)¬Evil(x)
¬∃x King(x)∧Evil(x)\neg\exists x\ King(x)\wedge Evil(x)¬∃x King(x)Evil(x)
∀x ¬(King(x)∧Evil(x))\forall x\ \neg(King(x)\wedge Evil(x))x ¬(King(x)Evil(x))(也对)
¬∀x King(x)∧Evil(x)\neg\forall x\ King(x)\wedge Evil(x)¬∀x King(x)Evil(x)(错)
最后一种只否定了"万物都是坏国王"

4.3 本体论与认识论承诺谱系(对应原书 Figure 8.1)

表达力(本体论承诺)由弱到强:

命题逻辑          →  事实
一阶逻辑          →  事实、对象、关系
时序逻辑          →  事实、对象、关系、时间
概率论            →  事实(+ 度量置信度)
模糊逻辑          →  真值度介于 [0,1] 的事实

认识论承诺(对句子的信念状态):
命题/一阶/时序逻辑  →  true / false / unknown
概率论              →  [0,1] 区间的置信度
模糊逻辑            →  已知的区间值(度)

易混淆点

  • 概率论并没有比命题逻辑更强的本体论承诺——它只是对"事实"允许部分信念。
  • 一阶概率逻辑(如 Markov Logic Networks、第 15 章的关系概率模型)结合两者:对象+关系的本体论 + 概率的认识论。

4.4 项、原子句子、复合句子的层次结构

                    句子 (Sentence)
                    ┌────┴────┐
          原子句子              复合句子
       (AtomicSentence)     (ComplexSentence)
       ┌──────┴──────┐        ┌────┴────┐
   Predicate(...)   t₁ = t₂   连接词组合   量词句
       │                                   │
       └── 项 (Term) ─────────────┐   ∀x / ∃x + 句子
              ┌──────┬───────────┴┐
           常量     变量      Function(项,...)
          Richard    x         LeftLeg(Richard)

记忆要点

  • 项指称对象句子有真值
  • LeftLeg(Richard) 是项,没有真值
  • Brother(Richard, John) 是句子,有真值
  • 混淆两者是初学者的另一个常见错误。

4.5 数据库语义 vs 开放世界语义对比

场景 开放世界语义(标准 FOL) 数据库语义
KB 只有 Parent(John,Mary)Parent(John, Mary)Parent(John,Mary),问 Parent(John,Bob)Parent(John, Bob)Parent(John,Bob)? Unknown False(封闭世界)
常量 AAABBB 是否同一对象? Unknown,除非断言 不同(唯一名称)
论域有多少对象? 任意多(可无限) 恰好等于常量数(域闭包)
典型应用 常识推理、数学、开放域 KB 关系数据库、Prolog、CSP
推理复杂度 半可判定 通常可判定

5. 与其他章节的关联

5.1 承前

章节 关联
第 2 章 表示谱系(原子 → 因子化 → 结构化)在此完成最后一跳;FOL 是"结构化表示"的典范
第 7 章 本章的全部动机来自命题逻辑的表达力不足;蕴涵、模型、可靠性、完备性等元概念在此原样复用,只是模型结构变复杂
第 6 章 CSP 数据库语义(唯一名称 + 封闭世界 + 域闭包)正是 CSP 的隐含假设;CSP 可看作数据库语义下的受限 FOL

5.2 启后

章节 关联
第 9 章 FOL 推理 本章只讲"怎么说",第 9 章讲"怎么算"。核心工具:unification(处理变量匹配)、lifted inference(避免命题化爆炸)、Herbrand 定理(连接 FOL 与命题逻辑)
第 10 章 知识表示 本章提供语言,第 10 章提供内容:上层本体、类别、事件、时空、心理事件。§3.8 的知识工程流程在第 10 章展开为本体工程
第 11 章 规划 PDDL 是 FOL 的受限片段(无量词嵌套、封闭世界、STRIPS 假设),用表达力换求解效率——本章 §3.2 讨论的经典权衡的实例
第 12 章 机器人 KR situation calculus 与 event calculus 都是 FOL 的特定使用方式:把"情境"或"事件"具体化(reification)为一等对象
第 15 章 关系概率模型 把 FOL 的对象/关系本体论与概率的认识论结合,得到 RPM / MLN / BLOG
第 19 章 归纳逻辑编程 从例子中学习 FOL 规则,是本章"手工写公理"的自动化对偶

5.3 具体化(Reification):贯穿后续章节的核心技巧

本章埋下的一个重要伏笔:把关系/事件/时间提升为对象

  • 想说"约翰在 5 点吃了苹果",若用 Eat(John,Apple,5)Eat(John, Apple, 5)Eat(John,Apple,5),则难以再添加"用叉子吃的"、“吃得很快”。
  • 事件具体化∃e Eating(e)∧Agent(e,John)∧Object(e,Apple)∧Time(e,5)∧Instrument(e,Fork)\exists e\ Eating(e)\wedge Agent(e,John)\wedge Object(e,Apple)\wedge Time(e,5)\wedge Instrument(e,Fork)e Eating(e)Agent(e,John)Object(e,Apple)Time(e,5)Instrument(e,Fork)
  • 这样每个修饰语只需加一个合取项,无需改变谓词的元数

这一技巧在第 10 章(事件演算)、第 12 章(situation/event calculus)中是绝对核心,也是语义网 RDF 三元组、知识图谱设计的理论基础。


6. 延伸思考

6.1 大语言模型有"一阶逻辑"的内部表示吗?

FOL 的核心承诺是:世界由离散对象及其关系构成。这个承诺在 Transformer 中是否成立?

观察到的现象

  • LLM 在关系组合上常出错。给定"A 是 B 的父亲,B 是 C 的父亲",问"A 与 C 的关系",模型多数能答对;但链条加长到 5–6 跳,准确率显著下降。这与 FOL 推理的"链式规则应用"形成对比——后者的正确性与链长无关
  • 反转诅咒(reversal curse):在"A is B"上训练的模型,往往无法推出"B is A"。而在 FOL 中,只要写下 ∀x,y Equal(x,y)⇔Equal(y,x)\forall x,y\ Equal(x,y)\Leftrightarrow Equal(y,x)x,y Equal(x,y)Equal(y,x),对称性对所有实例自动成立。这直指本章的核心优势:量化的普遍性(universally quantified generalization)。
  • 量词理解:LLM 对 ∀\forall/∃\exists 的嵌套顺序(“每人都爱某人” vs “有人被所有人爱”)常常混淆——这恰是 §2.5 中人类初学者也会犯的错。

开放性问题 1

Transformer 的注意力机制在结构上更接近"键值检索"(≈ 命题逻辑的模式匹配)还是"变量绑定"(≈ FOL 的 unification)?如果它缺乏真正的变量绑定机制(variable binding),那么无论参数多大,它能否学到"与实例无关的普遍规则"?

这不是纯理论问题。可验证的预测是:若模型缺乏变量绑定,则它在训练分布内表现优异,但对新对象(未见过的实体名)应用同一规则时会退化。这正是"组合泛化"(compositional generalization)研究的核心议题(SCAN、COGS 等基准)。

可能的调和路径

  • 神经符号混合:让 LLM 把自然语言翻译成 FOL(semantic parsing),交给定理证明器执行。已有系统(LINC、Logic-LM、SatLM)表明这条路线在逻辑基准上显著优于纯 CoT。
  • 在架构中显式加入绑定机制:如 Neural Turing Machine 的可寻址内存、Transformer 中的显式实体槽(entity slots)、Tensor Product Representation。

更深层的启示:FOL 的组合性(compositionality)——复合句的意义由其组成部分的意义决定——是符号系统的核心优势。Transformer 通过大规模预训练学到了统计上的"软组合性",但在处理系统性泛化(systematic generalization)时仍显不足。这提示我们:FOL 不仅是知识表示的语言,也是评估 AI 系统推理能力的试金石。

6.2 本体论承诺:多模态模型的"世界由什么构成"?

本章 §2.1 的框架可以直接用来审视多模态大模型:

系统 隐含的本体论承诺
FOL 离散对象 + 关系 + 函数
纯视觉 CNN 像素与特征图(无对象概念
目标检测器 有边界框的对象(有对象,关系弱
场景图(scene graph)模型 对象 + 二元关系(接近 FOL 的片段
视频/具身模型 对象 + 关系 + 时间(≈ 时序逻辑的本体论)

开放性问题 2

多模态模型要真正"理解"一个场景,是否必须在内部形成类似 FOL 的对象-关系结构?还是说分布式表示可以在不显式具体化对象的前提下达成等价的功能?

这触及认知科学的老问题(Fodor & Pylyshyn 的系统性论证 vs 联结主义回应)。但今天有了新的实证抓手:

  • 可解释性研究已在 LLM 中发现类似"实体追踪"的内部电路(entity tracking circuits)。
  • 若这些电路确实实现了近似的变量绑定,那么"符号结构可以从连续优化中涌现"就有了证据。

一个具体的思考实验

给多模态模型看一张有 20 个相同蓝色方块的图,问"最左边那个方块的右边第三个是什么颜色"。这需要对象个体化(individuation)——把视觉上不可区分的对象当作不同个体。FOL 通过唯一名称/等词天然支持(block1≠block2block_1 \neq block_2block1=block2 即便它们所有属性相同);而基于特征相似度的表示会天然把它们混淆。这类任务可作为"模型是否具备对象本体论"的探针。

6.3 AI 对齐视角:唯一名称假设与"身份"

一个容易被忽略但对齐相关的点:唯一名称假设(§2.7)在开放世界里是错误的

  • 同一个人可以有多个标识符(真名、笔名、账号、生物特征)。
  • AI 系统若默认"不同标识符 = 不同实体",会导致实体消解失败:无法把分散的信息聚合,或错误地把不同人合并。
  • 反过来,若系统能高效做跨源实体消解(entity resolution),就获得了去匿名化能力——这是显著的隐私风险。

开放性问题

在设计知识图谱与 Agent 记忆系统时,同一性判定的默认值应该是什么?采取"开放世界 + 不假设唯一名称"(保守,信息碎片化)还是"激进消解"(信息完整,隐私风险)?这不是纯技术选择,而是需要显式的价值权衡。

本章给出的技术工具(等词、唯一名称假设、开放/封闭世界)恰好是讨论这个问题的精确语言——这也再次说明:好的形式化不只帮助计算,也帮助我们把模糊的伦理直觉变成可讨论的命题

6.4 FOL 在现代知识图谱中的应用

一阶逻辑为现代知识图谱(Knowledge Graph, KG)和语义网(Semantic Web)提供了理论基础。虽然实际系统往往采用更受限的表示语言以换取可判定性和效率,但 FOL 的核心思想——对象、关系、量词——仍然是这些系统的设计蓝图。

FOL 与语义网标准的关系
标准/语言 与 FOL 的关系 表达能力
RDF (Resource Description Framework) FOL 的三元组片段subject-predicate-object 对应 Predicate(subject, object)。RDF 没有变量和全称量词,但通过 RDFS 和 OWL 扩展。 仅能表示二元关系(二元谓词)。
RDFS (RDF Schema) 添加了类(Class)、子类(subClassOf)、属性域/值域(domain/range)等公理模式。这些可视为 FOL 的特定公理模板。 有限的全称量词(通过 rdfs:subClassOf 等)。
OWL (Web Ontology Language) 描述逻辑(Description Logic) 的标准化,而描述逻辑是 FOL 的可判定子集。OWL 2 DL 对应 SROIQ(D)SROIQ(D)SROIQ(D) 描述逻辑。 支持全称/存在量词、类交并补、属性链、基数约束等,但禁止任意嵌套量词以保证可判定性。
SPARQL 知识图谱的查询语言,本质是图模式匹配,可视为对 FOL 存在量词查询的实现。 支持变量、连接、可选匹配(OPTIONAL ≈ 左外连接)。

关键设计权衡:语义网标准在 FOL 的表达力与计算复杂度之间做了明确取舍:

  • RDF:只保留原子句子(三元组),放弃变量和量词 → 查询效率高,但无法表达通用规则。
  • OWL:通过限制量词嵌套和函数符号,获得可判定性(通常是 EXPTIME 或 N2EXPTIME 复杂度),牺牲了 FOL 的完整表达能力(如任意函数、任意嵌套量词)。
FOL 在企业知识图谱构建中的角色
  1. 本体工程(Ontology Engineering)的规范语言

    • 设计阶段,知识工程师常用 FOL(或更易读的逻辑形式)来精确刻画领域概念、关系和约束。例如:
      ∀x (Employee(x) → ∃y (WorksFor(x, y) ∧ Company(y)))
      ∀x,y (ManagerOf(x, y) → (Employee(x) ∧ Employee(y) ∧ x ≠ y))
      
    • 这些 FOL 公理随后被"编译"为 OWL 公理(如 Employee ⊑ ∃WorksFor.Company),成为知识图谱的模式层(TBox)。
  2. 规则推理的底层语义

    • 许多知识图谱支持规则引擎(如 RIF、SWRL、Jena 规则),这些规则本质上是受限制的 FOL 子句(Horn 子句、Datalog)。
    • 例如,SWRL(Semantic Web Rule Language)规则:
      Parent(?x, ?y) ∧ Parent(?y, ?z) → Grandparent(?x, ?z)
      
      对应 FOL:∀x,y,z Parent(x,y)∧Parent(y,z)⇒Grandparent(x,z)\forall x,y,z\ Parent(x,y) \wedge Parent(y,z) \Rightarrow Grandparent(x,z)x,y,z Parent(x,y)Parent(y,z)Grandparent(x,z)
  3. 数据质量与一致性约束

    • FOL 可用于表达完整性约束(integrity constraints),在数据导入时检查一致性。例如"每个部门必须有且仅有一个经理":
      ∀d (Department(d) → ∃!m (ManagerOf(m, d)))
      
    • 在实际系统中,这类约束可能通过 SHACL(Shapes Constraint Language)或 OWL 的 owl:FunctionalPropertyowl:maxCardinality 来实现。
  4. 具体化(Reification)的模式设计

    • 如 §5.3 所述,具体化是处理 n 元关系的关键技术。在知识图谱中,这体现为将关系或事件本身作为节点
    • 例如,不用三元组 (John, ate, Apple),而用:
      :event1 rdf:type :EatingEvent .
      :event1 :agent :John .
      :event1 :object :Apple .
      :event1 :time "2023-10-01T12:00" .
      
      这直接对应 FOL 的具体化表示:∃e EatingEvent(e)∧agent(e,John)∧object(e,Apple)∧time(e,...)\exists e\ EatingEvent(e) \wedge agent(e,John) \wedge object(e,Apple) \wedge time(e,...)e EatingEvent(e)agent(e,John)object(e,Apple)time(e,...)
实践建议:何时用 FOL,何时用其子集?
场景 推荐技术 理由
需求分析、概念建模 FOL(或 UML/ER 图) 表达力最强,能无歧义地捕捉领域专家意图。
可扩展的企业级知识图谱 OWL 2 DL + SWRL 在表达力与可判定性间取得平衡,有成熟推理机(Pellet、HermiT、ELK)。
高性能规则推理(数亿三元组) Datalog / RDFox 线性时间数据复杂度,支持递归查询,适合大数据量。
需要自定义函数、算术运算 FOL + 外部谓词SHACL-SPARQL 纯 OWL 不支持自定义函数,需借助规则语言或约束语言。
临时性、探索性分析 SPARQL 查询 + 应用层代码 灵活,无需预先定义完整本体。

总结:FOL 是现代知识表示技术的理论基石。虽然工业级系统因性能考虑而采用其子集(描述逻辑、Datalog),但理解 FOL 的完整表达能力能让工程师更好地把握这些子集的能力边界,并在设计本体、编写规则时做出明智的权衡。正如本章开头所述,从命题逻辑到 FOL 是"从因子化到结构化"的质变;从 FOL 到其可判定子集,则是"从通用到实用"的工程化落地。

Logo

这里是“一人公司”的成长家园。我们提供从产品曝光、技术变现到法律财税的全栈内容,并连接云服务、办公空间等稀缺资源,助你专注创造,无忧运营。

更多推荐