谓词逻辑的等值和推理演算教学课件

主要内容谓词公式的等值等值演算范式(PNF,Skolem范式)推理式及推理演算归结推理1Lu Chaojun,SJTU 公式的等值谓词公式和如果在任一解释下都有相同的真值,就说和是等值等值的(或等价等价),记作 (或).定理 iff 是普遍有效的2Lu Chaojun,SJTU 由命题逻辑移植来的等值式在命题逻辑的等值式中以谓词公式代入命题变项,便可得谓词逻辑的等值式.例如:p p (x)P(x)(x)P(x)pq p q P(x)Q(x)P(x)Q(x)3 3Lu Chaojun,SJTU 量词转化型等值式量词的转化(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)例:(x)(Animal(x)Cat(x)并非动物都是猫=(x)(Animal(x)Cat(x)=(x)(Animal(x)Cat(x)存在不是猫的动物4 4Lu Chaojun,SJTU 量词分配等值式量词对及的分配律(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)其中 不含自由x!这个条件很容易满足:对约束变元改名即可.5 5Lu Chaojun,SJTU 量词分配等值式(续)量词对的分配律(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)其中 不含自由x!6 6Lu Chaojun,SJTU 量词分配等值式(续)对,对的分配律(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)(x)对,对没有分配律举例说明:(x)(Man(x)Woman(x)所有人要么是男人要么是女人.(x)Man(x)(x)Woman(x)要么所有人都是男人,要么所有人都是女人.7 7Lu Chaojun,SJTU 量词分配等值式(续)回顾:约束变元易名规则(x)(x)=(y)(y)(x)(x)=(y)(y)变元易名后的“分配律”(x)(y)(x)(y)=(x)(x)(x)(x)(x)(y)(x)(y)=(x)(x)(x)(x)8 8Lu Chaojun,SJTU 范式回顾:命题逻辑公式有与之等值的范式.谓词逻辑公式也有范式,其中前束范式与原公式是等值的,而其他范式与原公式只有较弱的关系.9Lu Chaojun,SJTU 前束范式定义:如果公式 中的所有量词都非否定地置于公式左端,且其辖域都延伸到公式的末端,则称是前束范式前束范式(prenex normal form).形如(Q1x1)(Qnxn)M(x1,xn)其中诸Qi为量词或,M不含量词,称为 的母式母式(基式基式,matrix).前束范式定理前束范式定理:任一公式都有与之等值的任一公式都有与之等值的PNF.10Lu Chaojun,SJTU 如何转化成PNF1.消去和2.否定词内移应用De Morgan律3.约束变元易名(如果必要的话)4.量词左移应用分配等值式11Lu Chaojun,SJTU 例:求PNF(x)(y)P(a,x,y)(x)(y)Q(y,b)R(x)=(x)(y)P(a,x,y)(x)(y)Q(y,b)R(x)=(x)(y)P(a,x,y)(x)(y)Q(y,b)R(x)=(x)(y)P(a,x,y)(x)(y)Q(y,b)R(x)=(x)(y)P(a,x,y)(y)Q(y,b)R(x)=(x)(y)P(a,x,y)(z)Q(z,b)R(x)=(x)(y)(z)(P(a,x,y)Q(z,b)R(x)=(x)(z)(y)(P(a,x,y)Q(z,b)R(x)=(x)(y)(z)(P(a,x,y)Q(z,b)R(x)(pp)1212Lu Chaojun,SJTU Skolem范式前束范式对前束量词没有次序要求,也没有其他要求.如果对前束范式进而要求所有都在之左,或者只保留而消去,便得Skolem范范式式的两种形式.13Lu Chaojun,SJTU Skolem范式(1):-前束范式一个公式的-前束范式形如(x1)(xi)(xi+1)(xn)M(x1,xn)是前束范式至少有一个存在量词存在量词都在全称量词的左边M(x1,xn)中不再有量词,也无自由个体变项14Lu Chaojun,SJTU-前束范式定理定理:任一公式都可化为-前束范式,并且 普遍有效 iff 普遍有效.说明:只有普遍有效的公式,才与其-前束范式是等值的.一般的公式与其-前束范式并不等值.用于FOL完备性的证明.15Lu Chaojun,SJTU 例:-前束范式求(x)(y)(u)P(x,y,u)的-前束范式(P中无量词).1.先求前束范式.本例已是.2.关键一步:(y)改写成(y).(z).形如(x)(y)(u)(P(x,y,u)S(x,y)(z)S(x,z)引入新谓词S和新变元z.(直观意义?)3.(z)左移即得结果:(x)(y)(u)(z)(P(x,y,u)S(x,y)S(x,z)当有多个在的左边,可按此法逐一右移.16Lu Chaojun,SJTU Skolem范式(2)PNF中消去所有而只保留.术语“Skolem范式”一般指这种形式.定理定理:任一公式任一公式 都可化为都可化为Skolem范式范式,并且并且 (不不)可满足可满足 iff (不不)可满足可满足.不是等值(equivalent),而是“等可满足”(equisatisfiable).17Lu Chaojun,SJTU 例:Skolem范式(x)(y)(z)(u)(v)(w)P(x,y,z,u,v,w)1.先求前束范式.本例已是.2.关键:消去.方法是引入个体常项或函数.如(y)(z)(u)(v)(w)P(a,y,z,u,v,w)消去x:引入新个体常项a代入x3.消去(u)时,引进的个体因为与左边的y和z有关,所以不能用个体常项,而是用函数(y)(z)(v)(w)P(a,y,z,f(y,z),v,w)4.消去(w):(y)(z)(v)P(a,y,z,f(y,z),v,g(y,z,v)18Lu Chaojun,SJTU 例:Skolem范式不保持等值比较(x)(y)P(x,y)与(x)P(x,f(x):在1,2域上(x)(y)P(x,y)=(P(1,1)P(1,2)(P(2,1)P(2,2)(x)P(x,f(x)=P(1,f(1)P(2,f(2)两者明显不等值.但在(不)可满足的意义下两者是一致的.19Lu Chaojun,SJTU 谓词逻辑的推理命题逻辑中有关推理形式、重言蕴涵以及基本的推理公式的讨论和所用的术语都可引入到谓词逻辑中,并可把命题逻辑的推理作为谓词逻辑的推理的一个部分来看待.这里我们讨论谓词逻辑所特有的推理形式和基本推理公式.20Lu Chaojun,SJTU 推理形式推理形式是指(用)表达推理的公式.推理形式表达的推理有正确的也有错误的.例1:所有整数都是有理数,所有有理数都是实数,所以所有整数都是实数.将这三句话形式化表示,可得如下推理形式:(x)(Integer(x)Rational(x)(x)(Rational(x)Real(x)(x)(Integer(x)Real(x)这是正确的推理形式在命题逻辑里只能表达成p q r,显然不是正确的推理形式.21Lu Chaojun,SJTU 推理形式:更多例子例2:人皆有死,孔子是人,所以孔子有死.(x)(Man(x)Mortal(x)Man(Confucius)Mortal(Confucius)例3:若有一个又高又胖的人,则有一个高个子而且有一个胖子.(x)(Tall(x)Fat(x)(x)Tall(x)(x)Fat(x)例4:若某个体a具有性质E,那么所有个体x都具有性质E.E(a)(x)E(x)这是错误的推理形式22Lu Chaojun,SJTU 基本推理式(1)(x)P(x)(x)Q(x)(x)(P(x)Q(x)(2)(x)(P(x)Q(x)(x)P(x)(x)Q(x)(3)(x)(P(x)Q(x)(x)P(x)(x)Q(x)(4)(x)(P(x)Q(x)(x)P(x)(x)Q(x)(5)(x)(P(x)Q(x)(x)P(x)(x)Q(x)(6)(x)(P(x)Q(x)(x)P(x)(x)Q(x)(7)(x)(P(x)Q(x)(x)(Q(x)R(x)(x)(P(x)R(x)(8)(x)(P(x)Q(x)P(a)Q(a)(9)(x)(y)P(x,y)(x)(y)P(x,y)(10)(x)(y)P(x,y)(y)(x)P(x,y)23Lu Chaojun,SJTU 举例说明基本推理式(2)(x)(P(x)Q(x)(x)P(x)(x)Q(x)语义说明:若个体域是某班学生,P(x)表示x是高材生,Q(x)表示x是运动健将,那么(x)(P(x)Q(x)表示有学生既是高材生又是运动健将,而(x)P(x)(x)Q(x)是说有高材生并且有运动健将(但不要求高材生和运动健将是同一个学生).显然推理式(2)成立.因为结论比前提弱,推理式(2)的逆不成立.24Lu Chaojun,SJTU 推理演算命题逻辑中的推理演算可推广到谓词逻辑.推理规则(代入规则需补充说明)都可直接移入谓词逻辑.除此之外,还需引入4条有关量词的推理规则.25Lu Chaojun,SJTU 消去规则消去规则:(x)(x)(y)y是个体变元,代表论域中任一个体.(y)是在(x)中对x代入y的结果.当(x)中不含量词和其他变项时成立.当允许(x)中出现量词和变项时,则需限制y不在(x)中约束出现.例如:(x)(z)(xz)在实数上成立,于是(z)(yz)也成立.但若将y取为z,便有(z)(zy)在实数域上成立,则(x)(z)(zx)也成立.但若引入(z),(z)(z)(zz)是不成立的.27Lu Chaojun,SJTU 消去规则消去规则:(x)(x)(c)其中c是未出现的个体常项如果存在个体使(x)为真,那么就让c是那个个体,自然(c)为真.这是数学里常用的存在推理法.需限制(x)(x)中没有自由个体变元出现.例如:实数域上(x)(xy)成立.由于y是自由个体变元,这时不能推导出cy.还需限制(x)中不含有c.例如在实数域上(x)(cx)是成立的,但c0)成立,但(x)(x)(xx)不成立.29Lu Chaojun,SJTU 使用中的注意事项多个量词下的量词消去与引入规则:(x)(y)(x,y)(y)(x,y)右端不能写成(y)(y,y)(x)(x,c)(y)(x)(x,y)右端不能写成(x)(x)(x,x)(x)(y)(x,y)(y)(x,y)(x,c)但不能再反推出(x)(x,c)和(y)(x)(x,y)原因是(x)(y)(x,y)成立时,对每个x所找到的y是依赖于x的,从而(x,y)的成立是有条件的,不是对所有的x都有同一个y.30Lu Chaojun,SJTU 推理演算在谓词逻辑里,真值表法不能使用,又不存在判明 普遍有效的一般方法.从而使用推理规则的推理演算是谓词逻辑的基本推理方法.推理演算过程:首先将以自然语句表示的推理问题形式化表示若不能直接使用基本的推理公式便消去量词,在无量词下使用规则和公式推理最后再引入量词31Lu Chaojun,SJTU 例:推理演算前提:(x)(P(x)Q(x),(x)(Q(x)R(x)结论:(x)(P(x)R(x)证明 (1)(x)(P(x)Q(x)前提 (2)P(x)Q(x)消去 (3)(x)(Q(x)R(x)前提 (4)Q(x)R(x)消去 (5)P(x)R(x)(2),(4)三段论 (6)(x)(P(x)R(x)引入32Lu Chaojun,SJTU 例:推理演算(续)人皆有死,苏格拉底是人,所以苏格拉底会死.令P(x):x是人,Q(x):x会死.于是问题可改述为(x)(P(x)Q(x)P(Socrates)Q(Socrates)证明 (1)(x)(P(x)Q(x)前提 (2)P(x)Q(x)消去 (3)P(Socrates)Q(Socrates)代入(4)P(Socrates)前提 (4)Q(Socrates)(3)(4)分离33Lu Chaojun,SJTU 例:推理演算(续)前提:(x)P(x)(x)(P(x)Q(x)R(x),(x)P(x)结论:(x)(y)(R(x)R(y)证明 (1)(x)P(x)(x)(P(x)Q(x)R(x)前提 (2)(x)P(x)前提 (3)(x)(P(x)Q(x)R(x)(1)(2)分离 (4)P(c)(2)消去 (5)(P(x)Q(x)R(x)(3)消去 (6)(P(c)Q(c)R(c)代入 (7)P(c)Q(c)(4)(8)R(c)(6)(7)分离 (9)(x)R(x)(8)引入 (10)(y)R(y)(8)引入 (11)(x)R(x)(y)R(y)(9)(10)(12)(x)(y)(R(x)R(y)(11)分配34Lu Chaojun,SJTU 例:推理演算(续)分析下面推理的正确性.(1)(x)(y)(x y)前提 (2)(y)(z y)消去 (3)z b 消去 (4)(z)(z b)引入 (5)b b 消去 (6)(x)(x x)引入从(1)到(2),应记住y是依赖于z的.从(2)到(3),b是依赖于z的.从(3)到(4)不成立:因为b是依赖于z的.从(5)到(6)也错:因为b是常项.35Lu Chaojun,SJTU 谓词逻辑的归结推理法归结证明法可推广到谓词逻辑,证明过程同命题逻辑,只不过要考虑量词和个体变元带来的复杂性.使用推理规则的推理演算灵活而技巧性强;归结法较为机械,容易使用计算机来 实现.36Lu Chaojun,SJTU 归结证明过程(1)回忆:为证明 ,可等价地证明 是矛盾式.(2)建立 的子句集S将G=化成等值的前束范式,进而化成Skolem范式(消去),得到仅含的公式G*.回忆:G不可满足性 iff G*不可满足再将G*中的省略,并将G*母式(已合取范式化)中的合取词以“,”表示,便得子句集S.S与G是同不可满足的S中的变元均被约束37Lu Chaojun,SJTU 归结证明过程(续)(3)对S进行一步归结:若S中有两个子句C1=L1 C1,C2=L2 C2,且对L1与L2有代入,使得两者合一合一(unification)L1=L2则可对其进行归结,得到归结式C1 C2,放入S中.(4)重复(3),直至得到矛盾式.38Lu Chaojun,SJTU 例:合一例如:设C1=P(x)Q(x),C2=P(a)R(y),对P(x)与P(a)进行变元代入=x/a后即可合一,从而可做归结.因此对C1和C2归结后得到归结式Q(a)R(y)39Lu Chaojun,SJTU 例:归结法证明(x)(P(x)Q(x)(x)(Q(x)R(x)(x)(P(x)R(x)1.改写成公式G:(x)(P(x)Q(x)(x)(Q(x)R(x)(x)(P(x)R(x)2.求G的子句集S:可分别对三个合取项求子句集,然后求其并集.(这样求得的子句集并非S,但与S是同不可满足的)(x)(P(x)Q(x)的子句集为P(x)Q(x)(x)(Q(x)R(x)的子句集为Q(x)R(x)(x)(P(x)R(x)=(x)(P(x)R(x)=(x)(P(x)R(x)经Skolem化得子句集P(a),R(a)于是得到G的子句集:P(x)Q(x),Q(x)R(x),P(a),R(a).40Lu Chaojun,SJTU 例:归结法证明(续)3.归结过程:(1)P(x)Q(x)(2)Q(x)R(x)(3)P(a)(4)R(a)(5)Q(a)(1)(3)归结 (6)R(a)(2)(5)归结 (7)空(矛盾)(4)(6)归结41Lu Chaojun,SJTU 作业习题5：1，4，5.4.27号交42Lu Chaojun,SJTU 43Lu Chaojun,SJTU End谢谢！