H.3 一阶逻辑

一阶逻辑（First-Order Logic，FOL）是一种灵活、成熟且计算上可处理的意义表示语言，满足 H.1 节提出的多项要求。它为可验证性、推理能力和表达能力提供了可靠的计算基础，也具有严格的模型论语义。FOL 对具体表示方式只作很少承诺，而这些承诺为许多其他体系所共有：被表示的世界由对象、对象的属性和对象之间的关系构成。

H.3.1 一阶逻辑的基本元素¶

FOL 用项（term）表示对象。项有三种形式：常量、函数和变量；它们都可以看作指定当前世界中的某个对象。

常量指向被描述世界中的特定对象，通常写作大写字母或首字母大写的词，如 $A$、$B$、$Maharani$ 和 $Harry$。一个常量只指称一个对象，但同一对象可以由多个常量指称。

函数常对应英语中的所有格概念，例如“Frasca 的位置”可以表示为：

函数在句法上类似单参数谓词，但它实际是项，指向唯一对象。函数使我们无需为每个对象另设命名常量，例如可方便地指称每家餐厅各自唯一的位置。

变量通常写作小写字母，使我们能够对对象作出断言和推理而不必指明某个命名对象。变量既可表示某个未知对象，也可泛指任意对象；量词使这两种用法成为可能。

谓词为论域中固定数量对象之间的关系命名。例如“Maharani 供应素食”可表示为：

二元谓词 $Serves$ 在两个常量所指称的对象之间成立。一元谓词则可断言单个对象的属性或类别成员关系：

项和谓词组成原子公式。逻辑连接词还可递归地把公式组成更大的表示。比如：

(H.20) 我只有五美元，而且我没有很多时间。

其意义由两个分句的语义以及 $\land$、$\neg$ 运算符组合而成。递归语法由有限规则生成无限多个逻辑公式。这里采用的 FOL 句法可概括为：

Formula       → AtomicFormula
              | Formula Connective Formula
              | Quantifier Variable,... Formula
              | ¬ Formula | (Formula)
AtomicFormula → Predicate(Term,...)
Term          → Function(Term,...) | Constant | Variable
Connective    → ∧ | ∨ | ⇒
Quantifier    → ∀ | ∃

图 H.3　一阶逻辑表示句法的上下文无关文法。 改编自 Russell 和 Norvig（2002）。

H.3.2 变量与量词¶

FOL 的两个基本量词是存在量词 $\exists$（“存在”）和全称量词 $\forall$（“对所有”）。英语中的不定名词短语往往提示存在量化。例如：

(H.22) ICSI 附近一家供应墨西哥菜的餐厅。

可表示为：

要使该公式为真，至少要有一个对象替换 $x$ 后使公式为真。若 AyCaramba 是 ICSI 附近的墨西哥餐厅，代入后得到：

三个原子公式全为真时，整个合取式为真；这些事实可以直接存在于知识库，也可以由其他事实推导出来。

全称量词要求用知识库中的任意对象替换变量后，公式都为真。例如：

(H.25) 所有素食餐厅都供应素食。

如果用 Maharani 替换 $x$，且已知它是素食餐厅并供应素食，则蕴含式为真。若用非素食餐厅 AyCaramba 替换，前件为假；依蕴含的真值表，整式仍为真。即使用 Carburetor 之类与餐厅无关的对象替换，前件仍为假，公式也保持为真。概括而言：公式中的变量必须受到存在量化或全称量化；存在量化只需至少一个使公式为真的替换，全称量化则要求所有替换都使公式为真。

H.3.3 Lambda 记号¶

lambda 记号（Church, 1940）可以从完全指定的 FOL 公式中抽象出形式参数，这对语义分析尤其有用。它把 FOL 扩展为如下表达式：

表达式由 $\lambda$、一个或多个变量以及使用这些变量的 FOL 公式组成。把 lambda 表达式应用于逻辑项，会把形式参数绑定到该项；随后通过文本替换并移除 $\lambda$，得到新的 FOL 表达式。该过程称为 $\lambda$-归约：

一个 lambda 表达式还可以作为另一个的主体：

先应用 $Bacaro$：

所得结果仍是 lambda 表达式；再应用 $Centro$：

这种把多参数谓词转换为一串单参数谓词的技术称为柯里化（currying；Schönfinkel, 1924）。lambda 记号还允许在谓词的参数没有同时作为句法树子节点出现时，逐步收集这些参数。

H.3.4 一阶逻辑的语义¶

FOL 知识库中的对象、属性和关系，凭借它们同外部世界中对象、属性和关系的对应而获得意义。H.2 节的模型论方法利用集合论概念，从意义表示表达式到被建模事态建立真值条件映射。

FOL 的项指称论域中的元素；原子公式中的一元属性可解释为论域元素集合，多元关系可解释为元素元组集合。例如：

(H.34) Centro 在 Bacaro 附近。

该公式的真值取决于：常量 $Centro$ 和 $Bacaro$ 所指称的元素组成的元组，是否属于谓词 $Near$ 所指称的关系集合。

含逻辑连接词的公式，其解释由各组成公式的意义与连接词的意义共同决定：

图 H.4　各逻辑连接词的真值表。 需要注意，逻辑“或”不完全等同于英语 or 的所有用法；蕴含 $\Rightarrow$ 同日常的因果或推断概念也只有较弱联系。

模型中只有论域元素及其关系，并没有变量。带变量公式的模型论解释通过替换来给出：含 $\exists$ 的公式，只要存在一个项的替换使公式在模型中为真即可；含 $\forall$ 的公式则必须在所有可能替换下都为真。

H.3.5 推理¶

意义表示语言必须支持推理：向知识库添加有效的新命题，或判断没有显式存储的命题是否为真。FOL 中最常实现的方法是肯定前件（modus ponens），也就是 if–then 推理。若蕴含式的前件为真，便可推出后件。抽象地说，若已知 $\alpha$ 与 $\alpha\Rightarrow\beta$，则可推出 $\beta$。

例如：

$VegetarianRestaurant(Leaf)$ 匹配规则前件，因此可以推出 $Serves(Leaf,VegetarianFood)$。

肯定前件可按两种方式使用。前向链推在事实加入知识库时触发所有适用的蕴含规则，把所得新事实继续加入知识库，直到无法推出更多事实。其优点是查询时所需事实往往已经存在，缺点是可能预先推导并存储永远不会用到的事实。

后向链推则从待证明的命题（查询）反向寻找事实。若查询不在知识库中，系统寻找后件能匹配该查询的规则，再递归证明规则前件。Prolog 就采用这种策略。例如，要证明 $Serves(Leaf,VegetarianFood)$，可以找到上面的规则，把 $Leaf$ 代入 $x$，再查询 $VegetarianRestaurant(Leaf)$；该命题正是已知事实。

必须区分“从查询回溯到已知事实”的后向链推，与“已知后件便假定前件”的逆向推理。若只知道 $Serves(Leaf,VegetarianFood)$，不能据此断言 $VegetarianRestaurant(Leaf)$；这种从后件到前件的推理称为溯因（abduction），它并不演绎有效，但在扩展语篇分析中常作为有用的合理推断。

前向链推和后向链推都是可靠的，却都不完备，即有些有效推论无法仅靠它们找到。归结（resolution）是可靠且完备的替代方法，但计算代价更高。实践系统因此通常采用某种链推方法，并要求知识库开发者以能够导出所需推论的形式编码知识。