第3章 确定性推理-2-Final

1、n若两个若两个WFF U及及V在任一解释下其值完全相同在任一解释下其值完全相同，则称这两个则称这两个WFF等价等价，表示为表示为 U V。n由于谓词逻辑是命题逻辑的推广由于谓词逻辑是命题逻辑的推广，命题逻辑命题逻辑中的基本等价式和推理规则在谓词逻辑仍可中的基本等价式和推理规则在谓词逻辑仍可沿用。但由于谓词逻辑中引入了变量及量词沿用。但由于谓词逻辑中引入了变量及量词，须再增加一些与变量须再增加一些与变量、量词有关的一些定理量词有关的一些定理和规则和规则，现现一并一并归纳归纳如如下下:3.1.4 谓词演算的等价式与永真蕴含式Basic equivalence formula and inferen

2、ce rule（1）双重否定律双重否定律(double negation law): (P(x) P(x)（2）德）德摩根定律摩根定律(Mogen law): (P(x)Q(x) P(x)Q(x)(P(x)Q(x) P(x)Q(x)（3）逆否律逆否律(inverse-negation law):P(x) Q(x) Q(x) P(x)（4）分配律分配律(assignment law):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)3.1.4 谓词演算的谓词演算的等价式与永真蕴含式Basic eq

3、uivalence formula and inference rule（5）结合律结合律(association law): （P(x) Q(x)R(x) P(x) (Q(x)R(x) （P(x) Q(x)R(x) P(x) (Q(x)R(x)（6）蕴含等价式蕴含等价式(implication law):P(x) Q(x) P(x) Q(x)（7）易名规则易名规则(rename law): x P(x) x Q(x) x P(x) y Q(y)（8）量词转换律量词转换律(quantifier transform law): x P(x) x P(x) x P(x) x P(x)3.1.4 谓

4、词演算的基本等价式及推理规则谓词演算的基本等价式及推理规则Basic equivalence formula and inference rule（9）量词分配律量词分配律(quantifier assignment law): x (P(x)Q(x) x P(x) x Q(x) x (P(x)Q(x) x P(x) x Q(x) x (P Q(x) P x Q(x) x (P Q(x) P x Q(x)（10）量词交换律量词交换律(quantifier commutative law): x y(P(x, y) y x(P(x, y) x y(P(x, y) ) y x(P(x, y) x

5、y(P(x, y) ) y x (P(x, y) x y (P(x, y) ) y x (P(x, y)3.1.4 谓词演算的谓词演算的等价式与永真蕴含式Basic equivalence formula and inference rule（11）量词辖域变换等价式量词辖域变换等价式: 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中不含变量中不含变量3.1.4 谓词演算的谓词演算的等价式与永真蕴含式Basic equivalence formula and inference rule3.1.4 谓

6、词演算的谓词演算的等价式与永真蕴含式Basic equivalence formula and inference rule（12）量词消去及引入规则量词消去及引入规则 全称量词消去规则全称量词消去规则: x P(x)P(y) 全称量词引入规则全称量词引入规则: P(y) x P(x) 存在量词消去规则存在量词消去规则: x Q(x)Q(c)(c 为常量为常量) 存在量词引人规则存在量词引人规则: Q(c) x Q(x) 有限域量词消去规则有限域量词消去规则:设有限个体域为设有限个体域为D d1，d2，dn x P(x)P(d1)P(d2)P(dn) x Q(x)Q(d1) Q(d2)Q(dn

7、)3.1.4 置换与合一置换与合一1. 置换n定义：形如t1/x1,t2/x2, tn/xn的一个有限集，其中，xi是变量，ti是不同于xi的项（常亮、变量、函数），且xi！=xj（i!=j）n空置换:n置换乘：n置换结合律成立，交换律不成立3.1.4 置换与合一置换与合一2. 合一 n定义：n最一般合一置换（mgu）:n定义n3个例子n谓词公式集的mgu不唯一nmgu的求解算法：n不一致集 例 E1：P（x, y, z）,E2: P(x, f(a), g(b)n算法：【板书】3.1.5 谓词逻辑中的范式谓词逻辑中的范式Normal form of predicate logicn同一个命题或

8、谓词公式可以用不同的命题或谓词同一个命题或谓词公式可以用不同的命题或谓词公式形式来表达公式形式来表达，这些公式形式之间是相互等值这些公式形式之间是相互等值的。的。n范式范式：公式的标准形式公式的标准形式，公式往往可以转换为和公式往往可以转换为和它等价的范式它等价的范式，以便对它们做一般性的处理。以便对它们做一般性的处理。n转换转换方法：方法：对给定公式中的某子公式用与它对给定公式中的某子公式用与它“等等价价”的一个公式来代替的一个公式来代替，并且重复该过程直到得并且重复该过程直到得出所需要的形式为止。下面给出一些定义。出所需要的形式为止。下面给出一些定义。F定义定义3.1 文字文字(liter

9、al)：是原子或原子之非。是原子或原子之非。F定义定义3.2 合取范式合取范式(conjunctive normal form)：当且仅当当且仅当G有形式有形式G1Gn (n=1)其中每个其中每个Gi都是文字的析取式。都是文字的析取式。F定义定义3.3 析取范式析取范式(disjunctive normal form)：当当且仅当且仅当G有形式有形式G1Gn(n=1)其中每个其中每个Gi都是文字的合取式。都是文字的合取式。 在命题逻辑中在命题逻辑中，若若P、Q、R是原子是原子，则则 P P、Q Q、R R、P P、Q Q、R R都是文字。都是文字。 是合取范式。是合取范式。 是析取范式。是析取

10、范式。() ()PQ RP Q() ( )P QPQR 3.1.5 谓词逻辑中的范式谓词逻辑中的范式Normal form of predicate logicF定理定理3.1 对任意公式对任意公式，都有与之等值的合取范都有与之等值的合取范式和析取范式。式和析取范式。 可按下述可按下述步骤步骤使用上一节中的等价式将使用上一节中的等价式将一个公式化为合取范式或析取范式。一个公式化为合取范式或析取范式。 (1) 使用等价式中的连接词化使用等价式中的连接词化简规律简规律消去公式消去公式中的连接词中的连接词 。 (2) 反复使用双重否定律和德反复使用双重否定律和德摩根律将摩根律将“”移到原子之前。移到

11、原子之前。 (3) 反复使用分配律和其他定律得出一个标准反复使用分配律和其他定律得出一个标准型。型。n在一阶逻辑中在一阶逻辑中，为了简化定理证明程序需要为了简化定理证明程序需要引入所谓的引入所谓的“前束标准型前束标准型”。,3.1.5 谓词逻辑中的范式谓词逻辑中的范式Normal form of predicate logic定义定义3.4 前束范式前束范式(prenex normal form)：设设F为一谓词公式为一谓词公式，如果其中的如果其中的所有量词均非否所有量词均非否定地出现在公式的最前面定地出现在公式的最前面，而它们的而它们的辖域为整个辖域为整个公式公式，则称则称F为为前束范式前束

12、范式(prenex normal form)。一般地一般地，前束范式可以写成前束范式可以写成: 其中其中 为为前缀前缀， 是一个由是一个由全称量词或存在量词组成的全称量词或存在量词组成的量词串量词串， 为为母式母式，它是一个不含任何量词的谓词公式。，它是一个不含任何量词的谓词公式。1 11()()( ,.,)nnnQxQ x M xx(1,2,., )iQ in1 1()()nnQ xQ x1( ,.,)nM xx3.1.5 谓词逻辑中的范式谓词逻辑中的范式Normal form of predicate logic 下面是一些前束范式的例子下面是一些前束范式的例子： 为了把一个公式化为前束范

13、式，需为了把一个公式化为前束范式，需要对上一节的等价式扩充，使之包含一要对上一节的等价式扩充，使之包含一阶逻辑特有的等价式对，如下所示。阶逻辑特有的等价式对，如下所示。 ()()( ( , )( )()()( , )( )()()()( ( , )( )xy P x yQ yxyP x yQ yxyz P x yQ z3.1.5 谓词逻辑中的范式谓词逻辑中的范式Normal form of predicate logic(1)() ( )()( ( )Qx F xGQx F xG(2)() ( )()( ( )Qx F xGQx F xG1212(3)() ( ) () ( ) ()()( (

14、 )( )Qx F xQx H xQx Qz F xH z1212(4)() ( ) () ( ) ()()( ( )( )Qx F xQx H xQx Qz F xH z在上述等价公式对中在上述等价公式对中， 和和 都表示含未量都表示含未量化变量化变量x的公式的公式， 表示不含未量化变量表示不含未量化变量x的公的公式式， 、 或为或为 或为或为 。对。对(3)和和(4)，要求要求z不出不出现在现在 中，中， 并且符合约束变量的换名原则。并且符合约束变量的换名原则。 ( )F x( )H xG1Q2Q( )F x3.1.5 谓词逻辑中的范式谓词逻辑中的范式Normal form of pred

15、icate logic一阶逻辑特有的等价式一阶逻辑特有的等价式：使用前面定义的等价式使用前面定义的等价式，总可以把一个公式化为总可以把一个公式化为前束标准型前束标准型。变换过程如下。变换过程如下。(1) 使用等价式中的连接词化使用等价式中的连接词化简规简规律消去公式中律消去公式中的连接词的连接词 、 。(2) 反复使用双重否定律和德反复使用双重否定律和德摩根律将摩根律将“”移移到原子之前。到原子之前。(3) 必要时重新命名量化的变量。必要时重新命名量化的变量。(4) 使用量词分配律和等价式使用量词分配律和等价式，把所有量词都移把所有量词都移到整个公式的最左边以得出一个范式。到整个公式的最左边以

16、得出一个范式。 3.1.5 谓词逻辑中的范式谓词逻辑中的范式Normal form of predicate logic提纲提纲n3.1 一阶谓词逻辑基础n1. 谓词逻辑的符号体系n2. 谓词逻辑的演算公式n3. 谓词公式的解释n4. 谓词演算的等价式与永真蕴含式n5. 谓词逻辑中的范式n3.2 谓词逻辑的演绎推理n3.3 命题逻辑的归结3.2 谓词逻辑的演绎推理方法谓词逻辑的演绎推理方法Deductive inference method of FOLn在传统的智能系统在传统的智能系统，特别是定理证明系统中特别是定理证明系统中，采采用最多的是用最多的是以形式逻辑为基础以形式逻辑为基础的演绎推

17、理。的演绎推理。下面下面主要介绍以一阶谓词逻辑为基础进行逻辑演绎推主要介绍以一阶谓词逻辑为基础进行逻辑演绎推理的基本方法和规则。理的基本方法和规则。1.推理形式推理形式(form of inference)n若在使谓词公式若在使谓词公式P=P1P2Pn为真的任一解为真的任一解释下释下，均有另一谓词公式均有另一谓词公式R为真为真，就说就说由由P推出了推出了R，P为为R的前提的前提，R为为P的逻辑结论的逻辑结论，用逻辑符号用逻辑符号表示为表示为P R或或PR。换言之，换言之，P R当且仅当当且仅当(1) P1P2Pn R是有效的是有效的；(2) P1P2Pn R是不可满足的。是不可满足的。 逻辑演

18、绎推理逻辑演绎推理就是使用就是使用推理规则推理规则证明公式证明公式P1P2Pn R是否成立。是否成立。3.2 谓词逻辑的演绎推理方法谓词逻辑的演绎推理方法Deductive inference method of FOL2.推理规则推理规则(rule of inference)n前提及结论引前提及结论引入入规则规则（P规则）规则） 在推理过程中可随时引入前提在推理过程中可随时引入前提，并把推理得到的中并把推理得到的中间结论作为后继推理的前提。间结论作为后继推理的前提。n替换规则替换规则（T规则）规则） 谓词公式中任一部分公式都可用其等价的公式替换。谓词公式中任一部分公式都可用其等价的公式替换。

19、n假言推理规则假言推理规则（CP规则）规则） 已知谓词公式已知谓词公式P Q及及P，则可推出公式则可推出公式Q。3.2 谓词逻辑的演绎推理方法谓词逻辑的演绎推理方法Deductive inference method of FOL3.推理过程推理过程(procedure of inference) 推理过程就是反复使用谓词演算的基本等价式及推理过程就是反复使用谓词演算的基本等价式及推理规则推理规则，对已知谓词公式进行变换对已知谓词公式进行变换，以得到所以得到所需逻辑结论的过程。需逻辑结论的过程。例例3.4 设已知如下事实：设已知如下事实：（1）只要是需要室外活动的课，郝亮都喜欢；）只要是需要室

20、外活动的课，郝亮都喜欢；（2）所有的公共体育课都是需要室外活动的课；）所有的公共体育课都是需要室外活动的课；（3）篮球是一门公共体育课。）篮球是一门公共体育课。求证：郝亮喜欢篮球这门课。求证：郝亮喜欢篮球这门课。3.2 谓词逻辑的演绎推理方法谓词逻辑的演绎推理方法Deductive inference method of FOLn证明：首先定义谓词及常量证明：首先定义谓词及常量Outdoor(x)x是需要室外活动的课；是需要室外活动的课；Like(x,y)x喜欢喜欢y；Sport(x)x是一门公共体育课；是一门公共体育课；hao郝亮，郝亮，basketball篮球篮球n把上述已知事实及待求解问

21、题用谓词公式表示如下：把上述已知事实及待求解问题用谓词公式表示如下：(1)Outdoor(x)Like(hao,x)(2)( x)(Sport(x)Outdoor(x)(3)Sport(basketball)(4)Like(hao,basketball) 待求证待求证3.2 谓词逻辑的演绎推理方法谓词逻辑的演绎推理方法Deductive inference method of FOLn应用推理规则进行推理应用推理规则进行推理(1)( x)(Sport(x)Outdoor(x) P规则规则(2) Sport(y)Outdoor(y) T规则规则(3) Sport(basketball),Spor

22、t(y)Outdoor(y) Outdoor(basketball) P规则及规则及CP规则规则(4) Outdoor(basketball) ,Outdoor(x)Like(hao,x) Like(hao,basketball) T规则及规则及CP规则规则3.2 谓词逻辑的演绎推理方法谓词逻辑的演绎推理方法Deductive inference method of FOL3.3 命题逻辑中的归结法命题逻辑中的归结法Resolution method in propositional logicn问题：问题：n给定给定命题逻辑描述的命题命题逻辑描述的命题F F1，F2 ,Fn和和G,G,n证明

23、证明在在F F1F2Fn成立的条件下有成立的条件下有G G成立成立？n或或证明：证明：F F1F2Fn G G是是定理定理( (重言式重言式) )？n分析：分析：n上述问题上述问题等价于等价于证明：证明：nF F1F2FnG G是矛盾是矛盾( (永假永假) )式式。n方法：反演推理方法：反演推理方法方法n从从F F1F2FnG G出发出发，使用归结使用归结原理原理来寻找来寻找矛盾矛盾，最后证明定理最后证明定理F F1F2Fn G G成立成立3.3.1 子句与子句与子句集子句集 Clause and clause setn把把F1F2FnG化成一种称作化成一种称作子句形子句形的的标准标准形式形式

24、n归结推理规则所应用的对象归结推理规则所应用的对象：子句子句(Clause)n子句子句：一组文字的析取一组文字的析取n一个文字或是一个原子一个文字或是一个原子(这时也称为正文字这时也称为正文字)，或者是一个原子的否定或者是一个原子的否定(这时也称为负文字这时也称为负文字)，n例例-文字文字： n例例-子句子句：P QR、P QR 例如例如，对如下，对如下公式公式 建立子句集建立子句集: 转换为如下的合取范式转换为如下的合取范式:n一个一个公式公式的的合取范式合取范式(CNF形式形式)常常表示为常常表示为一个一个子句的集合子句的集合。 ,SPRQR P ()()PQRP( ) ()PRQR P

25、S为为公式的子句集公式的子句集，其中其中每个元素都是一个子句每个元素都是一个子句。建立子句集建立子句集S：3.3.2 归结式归结式Resolventn命题逻辑的归结命题逻辑的归结原理原理 ： 设有两个子句设有两个子句: (其中其中 、 是子句是子句, 是文字是文字),从中消去互补对从中消去互补对(即即 和和 ),所所得的新子句得的新子句: ，便称作子句便称作子句 ， 的归结式的归结式，原子原子 称为被归结的原子。称为被归结的原子。n这个过程称为归结。这个过程称为归结。n没有互补对的两没有互补对的两个个子句没有归结式。子句没有归结式。n综上，综上，归结推理归结推理是是对两对两个个子句做归结子句做归结，即求归结式即求归结式R(C1，C2)的过程的过程。n问题：上述归结是否合理？问题：上述归结是否合理？P1122,CP C CP C1C2CP P1212( ,)RC CCC1C2CP定理定理3.2 子句子句C1和和C2的归结式是的归结式是C1和和C2的逻辑推论的逻辑推论，即即C1 C2