3.与或图的F规则变换
 　　这些规则是建立在某个问题辖域中普通陈述性知识的蕴涵公式基础上的。我们把允许用作规则的公式类型限制为下列形式：
LW
式中：L是单文字；W为与或形的唯一公式。我们也假设出现在蕴涵式中的任何变量都有全称量化作用于整个蕴涵式。这些事实和规则中的一些变量被分离标准化，使得没有一个变量出现在一个以上的规则中，而且使规则变量不同于事实变量。单文字前项的任何蕴涵式，不管其量化情况如何都可以化为某种量化辖域为整个蕴涵式的形式。这个变换过程首先把这些变量的量词局部地调换到前项，然后再把全部存在量词Skolem化。
　　举例说明如下：公式 (x){[(y)(z)P(x,y,z)](u)Q(x,u}
可以通过下列步骤加以变换：
　　(1) 暂时消去蕴涵符号 (x){～[(y)(z)P(x,y,z)]∨(u)Q(x,u)}
　　(2) 把否定符号移进第一个析取式内，调换变量的量词 (x){(y)(z)[～P(x,y,z)]∨(u)Q(x,u)}
　　(3) 进行Skolem化 (x){(y)[～P(x,y,f(x,y))]∨(u)Q(x,u)}
　　(4) 把所有全称量词移至前面然后消去 ～P(x,y,f(x,y))∨Q(x,u)
　　(5) 恢复蕴涵式 P(x,y,f(x,y))Q(x,u)

　　以下用一个自由变量的命题演算情况来说明如何把这类规则应用于与或图。
　　把形式为LW的规则应用到任一个具有叶节点n并由文字L标记的与或图上，可以得到一个新的与或图。在新的图上，节点n由一个单线连接符接到后继节点(也由L标记)，它是表示为W的一个与或图结构的根节点。作为例子，考虑把规则S(X∧Y)∨Z应用到图4.5所示的与或图中标有S的叶节点上。所得到的新与或图结构表示于图4.6，图中标记S的两个节点由一条叫做匹配弧的弧线连接起来。
　　在应用某条规则之前，一个与或图(如图4.5)表示一个具体的事实表达式。其中，在叶节点结束的一组解图表示该事实表达式的子句形。我们希望在应用规则之后得到的图，既能表示原始事实，又能表示从原始事实和该规则推出的事实表达式。











图4.6 应用一条规则得到的与或图
　　假设我们有一条规则LW，根据此规则及事实表达式F(L)，可以推出表达式F(W)。F(W)是用W代替F中的所有L而得到的。当用规则LW来变换以上述方式描述的F(L)的与或图表示时，我们就产生一个含有F(W)表示的新图；也就是说，它是以叶节点终止的解图集以F(W)子句形式代表该子句集。这个子句集包括在F(L)的子句形和LW的子句形间对L进行所有可能的消解而得到的整集。
　　再讨论图4.6的情况。规则S[(X∧Y)∨Z]的子句形是：
　　　　～S∨X∨Z
和
　　　　～S∨Y∨Z
　　　　[(P∨Q)∧R]∨[S∧(T∨U)]的子句形解图集为
　　　　P∨Q∨S
　　　　R∨S
　　　　P∨Q∨T∨U
　　　　R∨T∨U
应用两个规则子句中任一个对上述子句形中的S进行消解：

以及

于是我们得到4个子句对S进行消解的消解式的完备集为：
　　　　　　　　　　　　　　　　　　　　　　　　　　X∨Z∨P∨Q
　　　　　　　　　　　　　　　　　　　　　　　　　　Y∨Z∨P∨Q
　　　　　　　　　　　　　　　　　　　　　　　　　　R∨X∨Z
　　　　　　　　　　　　　　　　　　　　　　　　　　R∨Y∨Z
这些消解式全部包含在图4.4的解图所表示的子句之中。
　　从上述讨论我们可以得出结论：应用一条规则到与或图的过程，以极其经济的方式达到了用其它方法要进行多次消解才能达到的目的。
　　我们要使应用一条规则得到的与或图继续表示事实表达式和推得的表达式，这可利用匹配弧两侧有相同标记的节点来实现。对一个节点应用一条规则之后，此节点就不再是该图的叶节点。不过，它仍然由单一文字标记而且可以继续具有一些应用于它的规则。我们把图中标有单文字的任一节点都称为文字节点，由一个与或图表示的子句集就是对应于该图中以文字节点终止的解图集。

　　4.作为终止条件的目标公式

　　应用F规则的目的在于从某个事实公式和某个规则集出发来证明某个目标公式。在正向推理系统中，这种目标表达式只限于可证明的表达式，尤其是可证明的文字析取形的目标公式表达式。我们用文字集表示此目标公式，并设该集各元都为析取关系。(在以后各节所要讨论的逆向系统和双向系统，都不对目标表达式作此限制。)目标文字和规则可用来对与或图添加后继节点，当一个目标文字与该图中文字节点n上的一个文字相匹配时，我们就对该图添加这个节点n的新后裔，并标记为匹配的目标文字。这个后裔叫做目标节点，目标节点都用匹配弧分别接到它们的父辈节点上。当产生式系统产生一个与或图，并包含有终止在目标节点上的一个解图时，系统便成功地结束。此时，该系统实际上已推出一个等价于目标子句的一部分的子句。


图4.7 满足中终止条件的与或图

　　图4.7给出一个满足以目标公式(C∨G)为基础的终止条件的与或图，可把它解释为用一个“以事实来推理”的策略对目标表达式(C∨G)的一个证明。最初的事实表达式为(A∨B)。由于不知道A或B哪个为真，因此我们可以试着首先假定A为真，然后再假定B为真，分别地进行证明。如果两个证明都成功，那么我们就得到根据析取式(A∨B)的一个证明。而A或B到底哪个为真都无关紧要。图4.7中标有(A∨B)的节点，其两个后裔由一个2线连接符来连接。因而这两个后裔都必须出现在最后解图中，如果对节点n的一个解图通过k线连接符包含n的任一后裔，那么此解图必须包含通过这个k线连接符的所有k个后裔。
图4.7的例子证明过程如下：
　　　　　　　　　　　　　　　　　　事实：A∨B
　　　　　　　　　　　　　　　　　　规则：AC∧D，BE∧G
　　　　　　　　　　　　　　　　　　目标: C∨G
　　把规则化为子句形，得子句集：
　　　　　　　　　　　　　　　　　　～A∨C，～A∨D
　　　　　　　　　　　　　　　　　　～B∨E，～B∨G
目标的否定为:～(C∨G)
其子句形为:～C，～G
　　用消解反演来证明目标公式，如图4.8所示。
图 4.8 用消解反演求证目标公式的图解


 从图4.8我们推得一个空子句NIL，从而使目标公式(C∨G)得到证明。
　　我们得到的结论是：当正向演绎系统产生一个含有以目标节点作为终止的解图时，此系统就成功地终止。
　　对于表达式含有变量的正向产生式系统，我们考虑把一条(LW)形式的规则应用到与或图的过程，其中L是文字，W是与或形的一个公式，而且所有表达式都可以包含变量。如果这个与或图含有的某个文字节点L′同L合一，那么这条规则就是可应用的。设其最一般合一者为u，那么这条规则的应用能够扩展这个图。为此，建立一个有向的匹配弧，从与或图中标有L′的节点出发到达一个新的标有L的后继节点。这个后继节点是Wu的与或图表示的根节点，我们用mgu，或者简写为u来标记这段匹配弧。