第4章 经典逻辑推理(精品·公开课件).ppt

* 郑州大学振动工程研究所 4.3归结演绎推理(续） (6) ?I(x) ? ?L(x) S2 (1)与（3）归结 S2 : (7) ?L(a) (2)与（6）归结 (8) ?L(a) (3)与（5）归结 (9) ?I(a) (4)与（6）归结 S3: (10) NIL (2)与（9）归结 上述归结过程可以用P141页的图4-10来描述。 3、线性输入策略 线性归结是这样一种归结，首先从子句集中选取一个称为顶子句的子句C0 开始做归结，其次是归结过程中所得到的归结式Ci立即同另一子句Bi进行归结得归结式Ci+1。而Bi?S ? Ck(ki) (已出现过的归结式）。这里关键的问题是顶子句的选择，一般选择结论的否定作为顶子句。 * 郑州大学振动工程研究所 4.3归结演绎推理(续） 例如：证明P ?Q， ? P ?Q， P ? ? Q ? P ?Q 解，问题转化成证子句集合S={P ?Q， ? P ?Q， P ? ? Q ， ? P ? ? Q} 的不可满足问题，用线形消解的图解表示如下： * 郑州大学振动工程研究所 4.3归结演绎推理(续） 4、单文字子句策略 如果一个子句只包含一个文字，则称它为单文字子句。 单文字子句策略要求参加归结的两个子句中必须至少有一个是单文字子句。例子见P142页的例4.20.但单文字策略是不完备的，即当子句集合中不存在单文字子句时，不能使用单文字子句策略。 5、祖先过滤形策略 该策略与线性输入策略比较相似，它要求对两个子句进行消解时，只要它们满足下面两个条件之一就可进行归结。 （1）C1与C2中至少有一个是初始子句集中的子句。 （2）如果两个子句都不是初始子句集中的子句，则一个应是另一个的祖先。所谓C1是C2的祖先是指C2是由 C1和其它子句消解得到的消解式。 * 郑州大学振动工程研究所 4.3归结演绎推理(续） 例4.21设有子句集S={~P(x)vQ(x),~P(y)v~Q(y),P(u)vQ(u), P(t)v~Q(t)} 归结过程如下图所示： * 郑州大学振动工程研究所 4.3归结演绎推理(续） 以上我们讨论了归结演绎推理，它是在定理自动证明中影响较大的一种推理方法。它的缺点是要求把谓词公式转化成子句集，不便于理解，另外它还可能会丢失一些重要的控制信息。 针对归结演绎存在的上述问题，人们提出了多种非子句定理证明的方法，尼尔逊提出的基于与/或形的演绎推理就是其中的一种。 * 郑州大学振动工程研究所 4.4 与/或形演绎推理 归结演绎要求把相关问题的知识及问题的否定均转化成子句形式，然后通过归结演绎推理，其推理规则只有一条，即归结规则。与/或形演绎推理则是把领域知识及已知事实分别用蕴含式及与/或形表示出来，然后通过运用蕴含式进行演绎推理，从而证明某个目标公式。 与/或形演绎推理分别分为正向演绎、逆向演绎及双向演绎三种推理形式，下面分别介绍它们。 4.4.1与/或形正向演绎推理 在这种推理中，对已知事实、F规则及目标公式的表示形式都有一定的要求，如果不满足要求的形式就需要变换。 * 郑州大学振动工程研究所 4.4 与/或形演绎推理 1、事实表达式的与/或形变换及其树形表示 变换过程与化子句集类似，只是不必化为子句的合取形式，也不消去公式中的合取词。 2、F规则的表示形式 在与/或形正向演绎推理中，通常要求F规则具有如下的形式： L?W 其中，L是单文字，W是与/或形。 之所以要求F规则的左部为单文字，是因为在进行演绎推理时，要用F规则作用于表示事实的与/或树，而该与/或树的叶节点都是单文字，这样就可以用F规则的左部与叶节点进行简单匹配（合一）。 * 郑州大学振动工程研究所 4.4 与/或形演绎推理 如果领域知识不是上面的形式则通过等价变换变成规定的形式。例如对公式 （?x)(((?y)((?z)P(x,y,z))? (?u)Q(x,u))? （?x)( ~ ((?y)((?z)P(x,y,z))? (?u)Q(x,u)) ? (?x)( (?y) (?z) ~ P(x,y,z) ? (?u)Q(x,u)) ? (?x) (?y) (?z) (?u)(~ P(x,y,z) ? Q(x,u)) ? (?u)(~ P(x,y,f(x,y)) ? Q(x,u)) ? ~ P(x,y,f(x,y)) ? Q(x,u) ? P(x,y,f(x,y)) ? Q(x,u) * 郑州大学振动工程研究所 4.4 与/或形演绎推理 3、目标公式的表示形式 在与/或形正向推理中，要求目标公