图4.24是这个例子应用规则变换后得到的与或图,它有两个解图,对应的两个子句是 图4.24应用一条含有变量的规则后得到的与或图 一个解图是否是一致的,需要看该解图所涉及的若干个置换组成的置换集是否存在矛盾。当置换集没有矛盾存在时,称该置换集是一致的,也就是没有矛盾的,否则就是不一致的。只有当解图所涉及的置换集是一致的时,解图才是一致的。置换集一致的充分必要条件是该置换集存在合一复合。置换集的合一复合也是一个置换,表示的是置换集中所有置换"综合"以后的结果。 当一个与或图应用了好几条规则之后,推出的与或图将含有多个的匹配弧,这时任一解图可能有多于一个的匹配弧(对应的置换是u1,u2,…),因此在列写解图的子句集时,只考虑具有一致的匹配弧置换的那些解图(一致解图)。一个一致解图表示的子句是对得到的文字析取式应用一个合一复合的置换之后所得到的子句。 可以证明对一个置换集求合一复合的运算是可结合和可交换的(求置换的合成是不可交换的),因此一个解图对应的合一复合不依赖于构造这个解图时所产生的匹配弧的次序。再强调一下,我们要求一个解图具有一个一致匹配弧的置换集,这样该解图所对应的子句才是从初始事实表达式和规则公式集推出的子句。 |