量词的推理规则

9.1.1 量词的推理规则

我们首先从全称量词开始。假定我们的数据库包含了标准的民间传说公理，它认定所有贪婪的国王都是邪恶的：

那么看来相当可能推断出下列任何一个语句：

全称实例化（简写为UI）的规则说明，我们可以推断出任何用基项（没有变量的项）置换变量得到的语句[28]。为了形式化地书写推理规则，我们采用了第8.3节介绍的置换的概念。设SUBST(θ , α )表示把置换θ 用于α 的结果。则对于任何变量v和基项g的规则可以表示为：

例如，先前给出的三个语句可以由置换{x / John}、{x / Richard}和{x / Father(John)}得到。

存在量词相应的存在实例化规则稍微复杂一些。对任何语句α 、变量v和未出现在知识库的其它地方的常量符号k，

例如，从语句

∃x Crown(x) ∧ OnHead(x, John)

我们可以推断出语句

Crown(C1) ∧ OnHead(C1, John)

只要C1不在知识库的别处出现。基本上，存在语句说明存在某些满足条件的对象，实例化过程仅仅是给该对象命名。自然地，该名字不能已经属于另一个对象。数学提供了一个很好的例子：假设我们发现存在一个略大于2.71828的数，令x等于它，能够满足方程d(xy)/dy=xy。我们可以赋予该数一个名称，比如e，但是如果赋予的是一个已经存在的对象名，比如π，则是错误的。在逻辑中，新的名称称为Skolem常数。存在实例化是一种更一般过程的特例，这种一般过程称为Skolem化，我们将在第9.5节讨论。

存在实例化比全称实例化更加复杂，它在推理中也承担了稍微有些不同的角色。全称实例化可以多次应用从而获得许多不同的结果，而存在实例化只能应用一次，然后存在量化语句就可以被抛弃。例如，一旦我们添加了语句Kill(Murderer, Victim)，我们就不再需要语句 ∃x Kill(x, Victim)。严格地说，新知识库逻辑上并不等价于旧知识库，但只有在原始知识库可满足时，新的知识库才是可满足的，可以证明它们在这个意义上是推理等价的。