第三章2消解原理

13.4消解原理Resolutionprinciple2内容提要置换、合一子句集的求取9个步骤消解推理规则含有变量的消解式消解反演求解3谓词逻辑法（predicatelogic）谓词演算1.语法与语义2.连词和量词谓词公式1.定义2.合适公式的性质置换与合一1.置换2.合一算法4命题def:具有真假意义的语句命题的真值典型的命题●中国的首都是北京●太阳从西边出来真假1+1=10●一个命题不能同时既为真又为假,但可以在一定条件下为真在另一种条件下为假Bob’scarisred●每个句子是一个命题,不能拆散Mary’suncle●没有真假意义的语句不是命题5命题逻辑有较大的局限性无法描述客观事物的结构和逻辑特征不能把不同事物间的共同特征表述出来两个命题●Tomisastudent●Roseisastudent两个命题无法把两个人都是学生这一共同特征表示出来引出谓词逻辑6谓词STUDENT(tom)GREATER(5,3)谓词谓词名个体谓词名个体用于刻划个体的性质,状态或个体间的关系表示某个独立存在的事物或某个抽象的概念刻划了tom的身份特征刻划了两个个体5和3之间的”大于”关系●谓词名通常大写,个体名通常小写●谓词中包含的个体数目称为谓词的元数7谓词公式的定义原子谓词公式：用P(x1,x2,…,xn)表示一个n元谓词公式其中P为n元谓词，x1,x2,…xn为客体变量或变元。通常把P(x1,x2,…,xn)叫做谓词演算的原子公式，或原子谓词公式。分子谓词公式：可以用连词把原子谓词公式组成复合谓词公式，并把它叫做分子谓词公式。8连词和量词原子公式由若干谓词和个体组成,是谓词演算的基本块,用连词和量词将多个原子公式组合在一起,来表示复杂的含义.用连词来连接若干个谓词组成一个谓词公式,用量词来刻划谓词和个体的关系合取析取蕴含非~全称量词存在量词连词量词9合取（conjunction）就是用连词∧把几个公式连接起来而构成的公式。合取项是合取式的每个组成部分。例：LIKE(I，MUSIC)∧LIKE(I，PAINTING)(我喜爱音乐和绘画。)析取（disjunction）就是用连词∨把几个公式连接起来而构成的公式。析取项是析取式的每个组成部分。例：PLAYS(LILI，BASKETBALL)∨PLAYS(LILI，FOOTBALL)(李力打篮球或踢足球。)10蕴涵表示如果-那么的语句。用连词连接两个公式所构成的公式叫做蕴涵。例:RUNS(LIUHUA,FASTEST)WINS(LIUHUA,CHAMPION)(如果刘华跑得最快，那么他取得冠军)非（NOT）表示否定，～、┑均可表示。例：～INROOM(ROBOT，r2)(机器人不在2号房间内。)IFPTHENQ前项,左项后项,右式11全称量词(UniversalQuantifier)若一个原子公式P(x)，对于所有可能变量x都具有T值，则用(x)P(x)表示。例：(x)[ROBOT(x)COLOR(x,GRAY)](所有的机器人都是灰色的）(x)[Student(x)Uniform(x,Color)](所有学生都穿彩色制服)存在量词(ExistentialQuantifier)若一个原子公式P(x)，至少有一个变元X，可使P(X)为T值，则用(x)P(x)表示。例：(x)INROOM(x,r1)(1号房间内有个物体)量化变元(QuantifiedVariables)被量化了的变元x-约束变量。12置换与合一置换形如{t1/x1,t2/x2,…,tn/xn}的有限集合。其中，ti是项，xi是互不相同的变元；ti/xi表示用ti置换xi；不允许ti与xi相同，也不允许变元xi循环地出现在另一个tj中。合一设有公式集F={F1,F2,…Fn},若存在一个置换s使得F1s=F2s=…=Fns，则称s是公式集F的一个合一，且称F1,F2,…Fn是可合一的。置换是不可交换的最一般合一13置换举例设有表达式P[x,f(y),B]，对于置换：s1={z/x,w/y}s2={A/y}分别有：P[x,f(y),B]s1=P[z,f(w),B]P[x,f(y),B]s2=P[x,f(A),B]14合一者、最一般合一者举例设有表达式集{Ei}={P[x,f(y),B]，P[x,f(B),B]}，①该表达式集的合一者：s1={B/y}，s2={w/x,B/y}②s1={B/y}是该表达式集的最一般合一者。（为什么？）15基本概念：对谓词演算公式进行分解和化简，消去一些符号，以求得导出子句。消解原理(resolutionprinciple),也叫做归结原理。消解是一种可用于一定的子句公式的重要推理规则。一子句定义为由文字的析取组成的公式(一个原子公式和原子公式的否定都叫做文字)。当消解可使用时，消解过程被应用于母体子句对，以便产生一个导出子句。eg，如果存在某个公理E1∨E2和另一公理～E2∨E3，那么E1∨E3在逻辑上成立。这就是消解，而称E1∨E3为E1∨E2和～E2∨E3的消解式(resolvent)。任一谓词演算公式可以化成一个子句集。其变换过程由下列九个步骤组成16子句集的求取消去蕴涵符号减少否定符号的辖域对变量标准化消去存在量词skolem函数化为前束型把母式化为合取范式消去全称量词消去连词符号更换变量名称任何文字的析取式称为子句，由子句构成的集合称为子句集。任何一个谓词公式都可以通过应用等价关系和推理规则化为相应的子句集。17常用等价关系名称等价关系1双重否定律～（～P）←→P2蕴含律PQ←→～P∨Q3摩根定律～(P∨Q)←→～P∧～Q～(P∧Q)←→～P∨～Q4分配律P∧（Q∨R）←→（P∧Q）∨（P∧R）P∨（Q∧R）←→（P∨Q）∧（P∨R）5交换律P∧Q←→Q∧PP∨Q←→Q∨P18常用等价关系名称等价关系6结合律（P∧Q）∧R←→P∧（Q∧R）（P∨Q）∨R←→P∨（Q∨R）7逆否律PQ←→～Q～P8量词转换律～(x)P（x）←→(x)～P（x）～(x)P（x）←→(x)～P（x）9量词分配律(x)[P（x）∧Q（x）]←→(x)P（x）∧(x)Q（x）(x)[P（x）∨Q（x）]←→(x)P（x）∨(x)Q（x）10(x)P（x）←→(y)P（y）(x)P（x）←→(y)P（y）19(1)消去蕴涵符号只应用∨和～符号，以～A∨B替换A=B(2)减少否定符号的辖域每个否定符号～最多只用到一个谓词符号上，并反复应用狄·摩根定律。例如：～A∨～B代替～(A∧B)～A∧～B代替～(A∨B)(x){～A}代替～(x)A(x){～A}代替～(x)AA代替～(～A)20(3)对变量标准化在任一量词辖域内，受该量词约束的变量为一哑元(虚构变量)，它可以在该辖域内处处统一地被另一个没有出现过的任意变量所代替，而不改变公式的真值。合适公式中变量的标准化，意味着对哑元改名以保证每个量词有其自己唯一的哑元。21(4)消去存在量词Skolem函数:在公式(y)[(x)P(x,y)]中，存在量词是在全称量词的辖域内，我们允许所存在的x可能依赖于y值。令这种依赖关系明显地由函数g(y)所定义，它把每个y值映射到存在的那个x。这种函数叫做Skolem函数。如果用Skolem函数代替存在的x,我们就可以消去全部存在量词，并写成：(y)P(g(y),y)Skolem函数所使用的函数符号必须是新的，即不允许是公式中已经出现过的函数符号。22从一个公式消去一个存在量词的一般规则是以一个Skolem函数代替每个出现的存在量词的量化变量，而这个Skolem函数的变量就是由那些全称量词所约束的全称量词量化变量，这些全称量词的辖域包括要被消去的存在量词的辖域在内。如果要消去的存在量词不在任何一个全称量词的辖域内，那么我们就用不含变量的Skolem函数即常量。例如，(x)P(x)化为P(A)，其中常量符号A用来表示我们知道的存在实体。A必须是个新的常量符号，它未曾在公式中其它地方使用过。例如：(z)(y)(x)P(x,y,z)被{(y)P(g(y),y,A)}代替，其中g(y)为一Skolem函数。23(5)化为前束形到这一步，已不留下任何存在量词，而且每个全称量词都有自己的变量。把所有全称量词移到公式的左边，并使每个量词的辖域包括这个量词后面公式的整个部分。所得公式称为前束形。前束形公式由前缀和母式组成，前缀由全称量词串组成，母式由没有量词的公式组成，即前束形=(前缀)(母式)全称量词串无量词公式24(6)把母式化为合取范式任何母式都可写成由一些谓词公式和(或)谓词公式的否定的析取的有限集组成的合取。这种母式叫做合取范式。我们可以反复应用分配律。把任一母式化成合取范式。A∨{B∧C}化为{A∨B}∧{A∨C}(7)消去全称量词到了这一步，所有余下的量词均被全称量词量化了。同时，全称量词的次序也不重要了。因此，我们可以消去前缀，即消去明显出现的全称量词。25(8)消去连词符号∧用{(A∨B),(A∨C)}代替(A∨B)∧(A∨C)，以消去明显的符号∧。反复代替的结果，最后得到一个有限集，其中每个公式是文字的析取。任一个只由文字的析取构成的合适公式叫做一个子句。(9)更换变量名称可以更换变量符号的名称，使一个变量符号不出现在一个以上的子句中。例如，对于子集{～P(x)∨～P(y)∨P[f(x,y)],～P(x)∨Q[x,g(x)],～P(x)∨～P[g(x)]}，在更改变量名后，得到子句集：{～P(x1)∨～P(y)∨P[f(x1,y)],～P(x2)∨Q[x2,g(x2)],～P(x3)∨～P[g(x3)]}26化为子句集实例教材P7027消解推理规则假言推理合并重言式空子句（矛盾）三段论常用规则含有变量的消解式28消解推理规则令L1为任一原子公式，L2为另一原子公式；L1和L2具有相同的谓词符号，但一般具有不同的变量。已知两子句L1∨α和～L2∨β,如果L1和L2具有最一般合一者σ，那么通过消解可以从这两个父辈子句推导出一个新子句(α∨β)σ。这个新子句叫做消解式。它是由取这两个子句的析取，然后消去互补对而得到的。29从父辈子句求消解式的例子(a)假言推理(c)重言式(b)合并(a)假言30(d)链式(三段论)(e)空子句(矛盾)31含有变量的消解式为了对含有变量的子句使用消解规则，我们必须找到一个置换，作用于父辈子句使其含有互补文字。令父辈子句由｛Li｝和｛Mi｝给出，而且假设这两个子句中的变量已经分离标准化。设｛li｝是｛Li｝的一个子集，｛mi｝是｛Mi｝的一个子集，使得集｛li｝和｛～mi｝的并集存在一个最一般的合一者σ。消解两个子句｛Li｝和｛Mi｝，得到的新子句:{{Li}-{li}}σ∪{{Mi}-{mi}}σ就是这两个子句的消解式。32消解式的多种选择消解两个子句时，可能有一个以上的消解式，因为有多种选择｛li｝和｛mi｝的方法。不过，在任何情况下，它们最多具有有限个消解式。P[x,f(A)]∨P[x,f(y)]∨Q(y)和～P[z,f(A)]∨～Q(z)如果取{li}={P[x,f(A)]}，{mi}={～P[z,f(A)]}那么得到消解式:P[z,f(y)]∨～Q(z)∨Q(y)如果取{li}={Q(y)}，{mi}={～Q(z)}那么得到消解式:P[x,f(A)]∨P[x,f(y)]∨～P[y,f(A)]进一步消解得消解式为:P[y,f(y)]可见这两个子句消解一共可得4个不同的消解式，其中3个是消解P得到的，而另一个是由消解Q得到的。33对含有变量的子句使用消解的例子34消解推理常用规则35消解反演求解过程基本思想把要解决的问题作为一个要证明的命题，其目标公式被否定并化成子句形，然后添加到命题公式集中去,把消解反演系统应