4.2.2 规则逆向演绎系统
  基于规则的逆向演绎系统,其操作过程与正向演绎系统相反,即为从目标到事实的操作过程,从then到if的推理过程。
  1.目标表达式的与或形式
  逆向演绎系统能够处理任意形式的目标表达式。首先,采用与变换事实表达式同样的过程,把目标公式化成与或形,即消去蕴涵符号,把否定符号移进括号内,对全称量词Skolem化并删去存在量词。留在目标表达式与或形中的变量假定都已存在量词量化。例如,目标表达式
  (y)(x){P(x)[Q(x,y)∧[P(x)∧S(y)]]}
被化成与或形:
  P(f(y))∨{Q(f(y),y)∧[R(f(y))∨S(y)]}
式中,f(y)为一Skolem函数。
  对目标的主要析取式中的变量分离标准化可得:
P(f(z))∨{Q(f(y),y)∧[R(f(y))∨S(y)]}
应注意不能对析取的子表达式内的变量y改名而使每个析取式具有不同的变量。
  与或形的目标公式也可以表示为与或图。不过,与事实表达式的与或图不同的是,对于目标表达式,与或图中的k线连接符用来分开合取关系的子表达式。上例所用的目标公式的与或图如图4.7所示。在目标公式的与或图中,我们把根节点的任一后裔叫做子目标节点,而标在这些后裔节点中的表达式叫做子目标。
图 4.9 一个目标公式的与或图表示

  这个目标公式的子句形表示中的子句集可从终止在叶节点上的解图集读出:
P(f(z))
Q(f(y),y)∧R(f(y))
Q(f(y),y)∧S(y)
  可见目标子句是文字的合取,而这些子句的析取是目标公式的子句形。
  2.与或图的B规则变换
  现在让我们应用B规则即逆向推理规则来变换逆向演绎系统的与或图结构,这个B规则是建立在确定的蕴涵式基础上的,正如正向系统的F规则一样。不过,我们现在把这些B规则限制为:
WL
形式的表达式。其中,W为任一与或形公式,L为文字,而且蕴涵式中任何变量的量词辖域为整个蕴涵式。其次,把B规则限制为这种形式的蕴涵式还可以简化匹配,使之不会引起重大的实际困难。此外,可以把像W(L1∧L2)这样的蕴涵式化为两个规则WL1和WL2。
  3.作为终止条件的事实节点的一致解图
  逆向系统中的事实表达式均限制为文字合取形,它可以表示为一个文字集。当一个事实文字和标在该图文字节点上的文字相匹配时,就可把相应的后裔事实节点添加到该与或图中去。这个事实节点通过标有mgu的匹配弧与匹配的子目标文字节点连接起来。同一个事实文字可以多次重复使用(每次用不同变量),以便建立多重事实节点。
  逆向系统成功的终止条件是与或图包含有某个终止在事实节点上的一致解图。下面我们讨论一个简单的例子,看看基于规则的逆向演绎系统是怎样工作的。这个例子的事实、应用规则和问题分别表示于下:

事实:
  F1: DOG(FIDO);狗的名字叫 Fido
  F2: ~BARKS(FIDO);Fido是不叫的
  F3: WAGS TAIL(FIDO);Fido摇尾巴
  F4: MEOWS(MYRTLE);猫咪的名字叫Myrtle
规则:
  R1: [WAGS TAIL(x1)∧DOG(x1)] FRIENDLY(x1);摇尾巴的狗是温顺的狗
  R2: [FRIENDLY(x2)∧BARKS(x2)]AFRAID(y2,x2);温顺而又不叫的东西是不值得害怕的
  R3: DOG(x3) ANIMAL(x3);狗为动物
  R4: CAT(x4) ANIMAL(x4);猫为动物
  R5: MEOWS(x5) CAT(x5);猫咪是猫
问题:是否存在这样的一只猫和一条狗,使得这只猫不怕这条狗?
  用目标表达式表示此问题为:
(x)(y)[CAT(x)∧DOG(y)∧AFRAID(x,y)]
  图4.8表示出这个问题的一致解图。图中,用双线框表示事实节点,用规则编号R1、R2和R5等来标记所应用的规则。此解图中有八条匹配弧,每条匹配弧上都有一个置换。这些置换为{x/x5},{MYRTLE/x},{FIDO/y},{x/y2,y/x2},{FIDO/y}({FIDO/y}重复使用四次)。由图4.8可见,终止在事实节点前的置换为{MYRTLE/x}和{FIDO/y}。把它应用到目标表达式,我们就得到该问题的回答语句如下:
[CAT(MYRTLE)∧DOG(FIDO)∧AFRAID(MYRTLE,FIDO)]