《归结演绎推理》PPT课件.ppt

《《归结演绎推理》PPT课件.ppt》由会员分享，可在线阅读，更多相关《《归结演绎推理》PPT课件.ppt（40页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、1第第4 4章章 自自动动推理推理2第第4章章自自动推理推理4.1 4.1 引言引言4.2 4.2 自然演绎推理自然演绎推理4.3 4.3 归结演绎推理归结演绎推理-1-134.3 4.3 归结归结演演绎绎推理推理-1-14归结证明过程是一种归结证明过程是一种反驳程序反驳程序，即即：不是证不是证明一个公式是有效的明一个公式是有效的(valid)valid)，而是证明公式而是证明公式之非是不之非是不可满足的可满足的(dissatisfiable)(dissatisfiable)。这完全是这完全是为了方便为了方便，并且不失一般性。并且不失一般性。埃尔布朗埃尔布朗(Herbrand)(也称海明伦也称

2、海明伦)提出的埃提出的埃尔布朗论域和尔布朗论域和埃尔布朗定理埃尔布朗定理为自动定理证明为自动定理证明奠定了理论基础。鲁宾逊奠定了理论基础。鲁宾逊(Robinson)原理使原理使定理证明的机械化变为现实。定理证明的机械化变为现实。4.3 归结演绎推理归结演绎推理-15若欲证明前提条件若欲证明前提条件P可推导出结论可推导出结论Q，即证，即证明明 永真，永真，该问题的该问题的证明等价于证明等价于证明证明永假，即永假，即是不可满足的。是不可满足的。4.3 归结演绎推理归结演绎推理-16由由于于谓谓词词逻逻辑辑是是命命题题逻逻辑辑的的推推广广，命命题题逻逻辑辑中中的的基基本本等等价价式式和和推推理理规规

3、则则在在谓谓词词逻逻辑辑仍仍可可沿沿用用。但但由由于于谓谓词词逻逻辑辑中中引引入入了了变变量量及及量量词词，须须再再增增加加一一些些与与变变量量、量量词词有有关关的的一一些些定定理理和规则和规则，现现一并一并归纳于下归纳于下:4.3.1 Skolem4.3.1 Skolem标准型标准型7双重否定双重否定律律(doublenegationlaw):(P(x)P(x)德德摩根摩根定律定律(Mogenlaw):(P(x)Q(x)P(x)Q(x)(P(x)Q(x)P(x)Q(x)1 1、谓词演算的基本等价式、谓词演算的基本等价式8逆否律逆否律(inverse-negationlaw):P(x)Q(x)

4、Q(x)P(x)分配律分配律(assignmentlaw):P(x)(Q(x)R(x)(P(x)Q(x)(P(x)R(x)P(x)(Q(x)R(x)(P(x)Q(x)(P(x)R(x)1 1、谓词演算的基本等价式、谓词演算的基本等价式9结合律结合律(associationlaw):（P(x)Q(x)R(x)P(x)(Q(x)R(x)（P(x)Q(x)R(x)P(x)(Q(x)R(x)蕴含等价式蕴含等价式(implicationlaw):P(x)Q(x)P(x)Q(x)1 1、谓词演算的基本等价式、谓词演算的基本等价式10易名规则易名规则(renamelaw):xP(x)xQ(x)xP(x)yQ

5、(y)量词转换律量词转换律(quantifiertransformlaw):xP(x)xP(x)xP(x)xP(x)1 1、谓词演算的基本等价式、谓词演算的基本等价式11量词分配律量词分配律(quantifierassignmentlaw):x(P(x)Q(x)xP(x)xQ(x)x(P(x)Q(x)xP(x)xQ(x)x(PQ(x)P xQ(x)x(PQ(x)P xQ(x)1 1、谓词演算的基本等价式、谓词演算的基本等价式12量词交换律量词交换律(quantifiercommutativelaw):x y(P(x,y)y x(P(x,y)x y(P(x,y)y x(P(x,y)x y(P(x

6、,y)y x(P(x,y)x y(P(x,y)y x(P(x,y)1 1、谓词演算的基本等价式、谓词演算的基本等价式13量词辖域变换等价式量词辖域变换等价式:xP(x)Q x(P(x)Q)xP(x)Q x(P(x)Q)xP(x)Q x(P(x)Q)xP(x)Q x(P(x)Q)Q中不含变量中不含变量1 1、谓词演算的基本等价式、谓词演算的基本等价式14 全称量词消去规则全称量词消去规则:x P(x)P(y)全称量词引入规则全称量词引入规则:P(y)x P(x)存在量词消去规则存在量词消去规则:xQ(x)Q(c)(c为常量为常量)存在量词引人规则存在量词引人规则:Q(c)x Q(x)2 2、量词

7、消去及引入规则、量词消去及引入规则15有有限限域域量量词词消消去去规规则则:设设有有限限个个体体域域为为D d1，d2，dn x P(x)P(d1)P(d2)，P(dn)x Q(x)Q(d1)Q(d2)，Q(dn)2 2、量词消去及引入规则、量词消去及引入规则163 3、谓词逻辑中的范式、谓词逻辑中的范式同同一一个个命命题题或或谓谓词词公公式式可可以以用用不不同同的的命命题题或或谓谓词词公公式式形形式式来来表表达达，这这些些公公式式形形式式之之间间是是相相互互等等值值的的。为为了了把把这这些些公公式式规规范范化化，下下面面讨讨论论公公式范式问题。式范式问题。所所谓谓范范式式就就是是公公式式的的

8、标标准准形形式式，公公式式往往往往可可以以转转换换为为和和它它等等价价的的范范式式，以以便便对对它它们们做做一一般般性性的处理。的处理。方方法法是是：对对给给定定公公式式中中的的某某子子公公式式用用与与它它“等等价价”的的一一个个公公式式来来代代替替，并并且且重重复复该该过过程程直直到到得出所需要的形式为止。下面给出一些定义。得出所需要的形式为止。下面给出一些定义。17范式中的范式中的一些定义一些定义:定义定义4.1 文字文字(literal)是原子或原子之非。是原子或原子之非。定定 义义 4.2 公公 式式 G，当当 且且 仅仅 当当 G有有 形形 式式G1Gn(n=1)其其中中每每个个Gi

9、都都是是文文字字的的析析取取式式。则则G称称为为合合取取范范式式(conjunctive normal form)3 3、谓词逻辑中的范式、谓词逻辑中的范式18定定 义义 4.3 公公 式式 G称称 为为 析析 取取 范范 式式(disjunctive normal form)，逻逻辑辑公公式式的的标标准准化化(或或规规范范化化)，它它是是合合取取子子句句的的析析取取.当当且且仅仅当当G有有形形式式G1Gn(n=1)其其中中每每个个Gi都都是是文文字字的的合合取式取式。例如例如:在命题逻辑中，若在命题逻辑中，若P、Q、R是原子，则是原子，则 P、Q、R、P、Q、R都是文字。都是文字。(P QR

10、)(P Q)是合取范式。是合取范式。(PQ)(PQ R)是析取范式。是析取范式。3 3、谓词逻辑中的范式、谓词逻辑中的范式19定定理理4.14.1 对对任任意意公公式式，都都有有与与之之等等值值的的合合取取范范式式和析取范式。和析取范式。可可按按下下述述程程序序使使用用上上一一节节中中的的等等价价式式将将一一个个公式化为合取范式或析取范式。公式化为合取范式或析取范式。(1)(1)使使用用等等价价式式中中的的连连接接词词化化规规律律消消去去公公式式中的连接词中的连接词,。(2)(2)反反复复使使用用双双重重否否定定律律和和德德摩摩根根律律将将“”移到原子之前移到原子之前。(3)(3)反反复复使使

11、用用分分配配律律和和其其他他定定律律得得出出一一个个标标准型。准型。3 3、谓词逻辑中的范式、谓词逻辑中的范式20定定义义4.4设设F为为一一谓谓词词公公式式，如如果果其其中中的的所所有有量量词词均均非非否否定定地地出出现现在在公公式式的的最最前前面面，而而它它们们的的辖辖域域为为整整个个公公式式，则则称称F为为前前束束范范式式(prenexnormalform)。一一般般地地，前前束束范范式式可以写成可以写成:其其中中 为为前前缀缀，是是一一个个由由全全称称量量词词或或存存在在量量词词组组成成的的量量词词串串，为为母母式式，它它是是一一个个不含任何量词的谓词公式。不含任何量词的谓词公式。4

12、4、前束标准型、前束标准型n在一阶逻辑中在一阶逻辑中，为了简化定理证明程序需要引入为了简化定理证明程序需要引入所谓的所谓的“前束标准型前束标准型”。21下面是一些前束范式的例子下面是一些前束范式的例子：为了把一个公式化为前束范式，需要对上一节的等为了把一个公式化为前束范式，需要对上一节的等价式扩充，使之包含一阶逻辑特有的等价式对，如价式扩充，使之包含一阶逻辑特有的等价式对，如下所示。下所示。4 4、前束标准型、前束标准型22 在上述等价公式对中在上述等价公式对中，F(x)和和 H(x)都表示含都表示含未量化变量未量化变量x的公式的公式，G表示不含未量化变量表示不含未量化变量x的的公公式，式，Q

13、1,Q2 或为或为 或为或为。对对(3)和和(4)，要求要求z不出现在不出现在F(x)中，并且符中，并且符合约束变量的换名原则。合约束变量的换名原则。4 4、前束标准型、前束标准型23使使用用前前面面定定义义的的等等价价式式，总总可可以以把把一一个个公公式式化化为为前束标准型前束标准型。变换过程如下：变换过程如下：(1)使使用用等等价价式式中中的的连连接接词词化化归归律律消消去去公公式式中中的的连连接接词词 、。(2)反反复复使使用用双双重重否否定定律律和和德德摩摩根根律律将将“()”移移到到原原子之前。子之前。(3)必要时重新命名量化的变量。必要时重新命名量化的变量。(4)使使用用量量词词分

14、分配配律律和和等等价价式式，把把所所有有量量词词都都移移到到整整个个公公式的最左边以得出一个范式。式的最左边以得出一个范式。4 4、前束标准型、前束标准型245 5、SkolemSkolem标准化过程标准化过程Step1:化成前束范式化成前束范式:Step2:使用下述方法可以消去前缀中存在的所有量词：使用下述方法可以消去前缀中存在的所有量词：令令 是是 中出现的存在量词中出现的存在量词 。Case1:若在若在 之前不出现全称量词，则选择一个与之前不出现全称量词，则选择一个与M中中出现的所有常量都不相同的新常量出现的所有常量都不相同的新常量c，用，用c代替代替M中出现中出现的所有的所有xr，并且

15、由前缀中删去，并且由前缀中删去(Qrxr)。Case2:若在若在 之前出现全称量词之前出现全称量词 ，则选择一个，则选择一个与与M中出现的任一函数符号都不相同的新中出现的任一函数符号都不相同的新m元函数符号元函数符号f，用，用 代替代替M中的所有中的所有xr，并且由前缀中删去，并且由前缀中删去(Qrxr)。25例题例题例例4.1 化公式化公式为为Skolem标准型。标准型。按上述方法删去前缀中的所有存在量词之后得出的按上述方法删去前缀中的所有存在量词之后得出的公式称为合式公式的公式称为合式公式的Skolem标准型标准型。替代存在量化。替代存在量化变量的常量变量的常量c(视为视为0元函数元函数)

16、和函数和函数f称为称为Skolem函数。函数。26 在在公公式式中中，的的前前面面没没有有全全称称量量词词，的的前前面面有有全全称称量量词词 和和 ,在在 的的前前面面有有全全称称量量词词 ，和和 。所所以以，在在 中中，用用常常数数a代代替替x,用用二二元元函函数数f(y,z)代代替替u,用用三三元元函函数数g(y,z,v)代替代替w,去掉前缀中的所有存在量词之后得出去掉前缀中的所有存在量词之后得出Skolem标准型标准型：例题分析例题分析27SkolemSkolem标准型定理标准型定理定理定理:若若G是给定的公式是给定的公式,而相应的子句集为而相应的子句集为S,则则G是不可满足的当且仅当是

17、不可满足的当且仅当S是不可满足的是不可满足的推论：设推论：设G=G1 Gn,Si 是是 Gi的的Skolem标准标准型，令型，令S=Si Sn，则，则，G是不可满足的当是不可满足的当且仅当且仅当S是不可满足的。是不可满足的。P121定理证明定理证明284.3.2子句型子句型归结证明过程是一种反驳程序归结证明过程是一种反驳程序，即即：不是证明不是证明一个公式是有效的一个公式是有效的(valid)valid)，而是证明公式之非而是证明公式之非是不是不可满足的可满足的(dissatisfiable)(dissatisfiable)。这完全是为了方这完全是为了方便便，并且不失一般性。并且不失一般性。我

18、们知道我们知道，归结推理规则所应用的对象是命题归结推理规则所应用的对象是命题或谓词合式公式的一种特殊的形式或谓词合式公式的一种特殊的形式，称为子句。称为子句。因此在进行归结之前需要把合式公式化为子句因此在进行归结之前需要把合式公式化为子句式。式。294.3.2子句型子句型定义定义4.5：任何文字的析取式称为任何文字的析取式称为子句子句。例如例如PQPQ，P(x,F(x),y)Q(y)R(f(x)P(x,F(x),y)Q(y)R(f(x)都是子句。都是子句。定义定义4.6：不包含任何文字的子句称为不包含任何文字的子句称为空子句空子句空子句中不包含任何文字，不能被任何解释空子句中不包含任何文字，不

19、能被任何解释满足，所以空子句是永假的，不可满足的。满足，所以空子句是永假的，不可满足的。由子句构成的集合称为子句集。由子句构成的集合称为子句集。在谓词逻辑中，任何一个谓词公式都可以化成一在谓词逻辑中，任何一个谓词公式都可以化成一个子句集。个子句集。304.3.2子句型子句型n谓词公式化为子句集步骤谓词公式化为子句集步骤(1)消去蕴涵符号：利用等价谓词关系消去谓词公式中的蕴涵符“”和双条件符“”。(2)减少否定符号的辖域：利用下列等价关系把否定符号“”移到紧靠谓词的位置上。31(3)变量标准化：变量标准化：重新命名变元名，使不同量词约重新命名变元名，使不同量词约束的变元有不同的名字束的变元有不同

20、的名字(4)消去存在量词消去存在量词存在量词不出现在全称量词的辖域内，此存在量词不出现在全称量词的辖域内，此时只要用一个新的个体常量替换该存在量时只要用一个新的个体常量替换该存在量词的约束变元可消去存在量词词的约束变元可消去存在量词存在量词位于一个或多个全称量词的辖域存在量词位于一个或多个全称量词的辖域内，如：内，如：4.3.2子句型子句型324.3.2子句型子句型(5)将公式化为前束形将公式化为前束形:把全称量词移到公式左边，并使每个量词的辖把全称量词移到公式左边，并使每个量词的辖域包含这个量词后面的整个部分，所得的公式域包含这个量词后面的整个部分，所得的公式称为前束形称为前束形.(6)把母

21、式化为合取范式把母式化为合取范式:利用等价关系利用等价关系，把公式，把公式化为化为Skolem标准形。标准形。Skolem标准形的一标准形的一般形式是般形式是33 (7)消去全称量词与合取词消去全称量词与合取词。如如PQPQ可表示为子句集可表示为子句集:P P Q Q(8)更改变量名，有时称为变量分离标准化。更改变量名，有时称为变量分离标准化。对变元更名，使不同子句中的变元不同名对变元更名，使不同子句中的变元不同名4.3.2子句型子句型34例例4.2 将合式公式化为子句形。将合式公式化为子句形。例题例题35解：（1）消去蕴涵符号）消去蕴涵符号：这可以利用等价式：得到：x(P(x)yP(y)P(

22、f(x,y)yQ(x,y)P(y)（2）减少否定符号的辖域，把减少否定符号的辖域，把“”移到紧移到紧靠谓词的位置上：靠谓词的位置上：这可以利用下述等价式：例题例题36得到：得到：x(P(x)yP(y)P(f(x,y)yQ(x,y)P(y)（3）变变量量标标准准化化：重重新新命命名名变变元元名名，使使不不同同量量词约束的变元有不同的名字：词约束的变元有不同的名字：xP(x)yP(y)P(f(x,y)wQ(x,w)P(w)（4）消去存在量词：）消去存在量词：xP(x)yP(y)P(f(x,y)Q(x,g(x)P(g(x)例题例题37（5）化为前束形：）化为前束形：x yP(x)P(y)P(f(x,

23、y)Q(x,g(x)P(g(x)（6 6）把母式化为合取范式：）把母式化为合取范式：x yP(x)P(y)P(f(x,y)P(x)Q(x,g(x)P(x)P(g(x)（7 7）消去全称量词和合取连接词：）消去全称量词和合取连接词：P(x)P(y)P(f(x,y)P(x)Q(x,g(x)P(x)P(g(x)例题例题38（8）更更改改变变量量名名，有有时时称称为为变变量量分分离离标标准准化化。于是有：必必须须指指出出:一一个个子子句句内内的的文文字字可可以以含含有有变变量量，但但这这些些变变量量总总是是被被理理解解为为全全称称量量词词量量化化了了的的变变量。量。例题例题391.1.什什么么是是子子句句?什什么么是是子子句句集集?请请写写出出求求谓谓词词公式子句集的步骤公式子句集的步骤.2.2.P144,P144,习题习题4.44.4作业作业埃尔布朗定理埃尔布朗定理补充内容补充内容40Thanks For Your Attention下下 课课