从实例中抽取一般规则

19.3.1 从实例中抽取一般规则

EBL背后的基本思想是首先使用先验知识构造对观察的一个解释，然后建立一个针对能够使用相同的解释结构的一类情况的定义。这个定义为一条可以涵盖该类中所有情况的规则提供了基础。“解释”可以是一个逻辑证明，但是更一般地，它可以是步骤定义明确的任何推理或问题求解过程。关键是能够明确把这些相同步骤应用于其它情况的必要条件。

我们将在我们的推理系统中使用在第九章中描述的简单的反向链接理论证明机。Derivative(X2, X) =2X的证明树过于庞大而无法作为例子，因此我们使用一个更简单的问题来诠释一般化方法。设想我们的问题是要化简1 × (0+X)。知识基础包括如下规则：

Rewrite(1 × u, u)

Rewrite(0+u, u)

Μ

答案是X的证明如图19.7的上半部分所示。EBL方法实际上同时构造了两棵证明树。第二棵证明树使用一个经过变形的目标，树中将原始目标中的常量替换为变量。随着原始证明过程的进展，经过变形的证明过程也在逐步进行，使用完全相同的规则。这可能引起一些变量的实例化。例如，为了使用规则Rewrite(1× u, u)，子目标Rewrite(x × (y+z), v)中的变量x必须与1绑定。相似地，为了使用规则Rewrite(0+u, u)，子目标Rewrite(y+z, v')中的y必须与0绑定。一旦我们有了一般化的证明树，我们选取叶子节点（经过必要的绑定）形成一条用于目标谓词的一般规则：

Rewrite(1×(0+z),0+z)∧Rewrite(0+z,z)∧ArithmeticUnknown(z)

注意左侧的前两个条件完全不考虑z的取值。因此我们可以把它们从规则中去掉，得到：

图19.7 化简问题的证明树。第一棵树表示对原始问题实例的证明，从中我们可以得到：

第二棵树表示了把所有常量都替换成变量的一个问题实例的证明，从中我们可以得到各种其它规则

一般来说，如果条件对最终规则右侧的变量没有施加任何约束，那么它们就可以被丢弃，因为得到的规则仍为真而且效率更高。注意我们没有丢弃条件ArithmeticUnknown(z)，因为并非z的所有可能取值都是算术未知量。对于不是算术未知量的取值，可能要求不同形式的化简：例如，如果z是2 × 3，那么1×(0+(2×3))的正确化简将是6而不是2×3。

重申一下，基本的EBL过程是如下进行的：

① 给定一个实例，使用可用的背景知识，构造出一棵把目标谓词应用于实例的证明。

② 并行地，使用与原始证明相同的推理步骤，为经过变形的目标构造一棵一般化证明树。

③ 构造一条新的规则，其左侧由证明树的叶子节点组成，右侧是经过变形的目标（在根据一般化证明过程对变量进行必要的绑定之后）。

④ 丢弃任何与目标中的变量取值完全无关的条件。