一阶推理规则

9.2.1 一阶推理规则

“约翰（John）是邪恶的（evil）”的推理过程如下：寻找某个x，使得这个x是一个国王（king），而且x是贪婪的（greedy），然后推理出x是邪恶的。更一般地，如果有某个置换θ使蕴涵的前提和知识库中已有的语句完全相同，那么应用θ后，我们就可以断言蕴涵的结论。在本实例中，置换{x / John}就达到了这个目的。

实际上我们可以让推理步骤完成更多的工作。假设不知道 Greedy(John)，但是我们知道每个人都是贪婪的：则我们依然能够得出结论Evil(John)，因为我们知道约翰是一个国王（已知），而且约翰是贪婪的（因为每个人都是贪婪的）。我们要让这个过程可行，就要为蕴涵语句中的变量和待匹配语句中的变量寻找置换。在这个例子中，把置换{x / John, y / John}应用于蕴涵前提 King(x)、Greedy(x)和知识库语句King(John)、Greedy(y)，将会使得它们完全相同。因此，我们可以推导出蕴涵的结论。

可以把此推理过程表述为一条单独的推理规则，我们称之为一般化分离规则（Generalized Modus Ponens）：对于原子语句pi、pi' 和q，存在置换θ 使得SUBST(θ,pi’)=SUBST(θ,pi)，对所有的i都成立。

该规则共有n+1个前提：n个原子语句pi' 和一个蕴涵。结论就是将置换应用于后项q得到的结果。对于我们的例子：

p1' 是King(John)　　　　　　 p1是King(x)

p2' 是Greedy(John)　　　　　　p2是Greedy(x)

θ是{x/John,y/John}　　　　　 q是Evil(x)

SUBST(θ,q)是Evil(John)

很容易证明一般化分离规则是一个可靠的推理规则。首先，我们观察到，对任何语句 p（假设它们的变量已经全称量化）以及任何置换θ ，

p|=SUBST(θ,p)

这一个推论成立，其原因与全称实例化规则成立的原因相同。特别是对于满足一般化分离规则的条件的θ ，这一个推论成立。因此，从p1', … , pn' 中，我们可以推断出

SUBST(θ,p1')∧ … ∧ SUBST(θ,pn')

从蕴涵p1∧…∧pnq，我们可以推断出

现在，把一般化分离规则中的θ定义为SUBST(θ,pi')=SUBST(θ,pi)，对所有的i；因此，两条语句中的第一句正好匹配上第二句的前提。从而，SUBST(θ , q)遵从分离规则。

一般化分离规则是分离规则（Modus Ponens）的提升版本——它将分离规则从命题逻辑提高到一阶逻辑。我们将在本章的其余部分中看到，我们可以发展出第七章中介绍的前向链接、反向链接和归结算法的提升版本。提升推理规则相对于命题化的最关键优点是只做那些使得特定推理能进行下去的置换。一个潜在可能引起困惑的地方是，人们会觉得一般化分离规则不如分离规则通用（第7.5节）：分离规则允许任何单个α 出现在蕴涵式的左侧，而一般化分离规则中要求该语句的特殊格式。在它允许有任何数量的pi' 的意义上说，它是一般化的。