《前束范式谓词推理》PPT课件.ppt

12/5/2019,discretemath,谓词公式的标准化形式：前束范式prenexnormalform(PNF)前束合取范式前束析取范式,前束范式,12/5/2019,discretemath,在定理的机器证明中，需要消除谓词公式中的量词，因而需要将谓词公式中的量词前束化，即把公式中的量词均提取到公式的前部。即前束范式主要是对量词的位置有要求，而对联接词无要求，这一点与命题逻辑不同。,前束范式作用,12/5/2019,discretemath,定义：一个谓词公式，如果它的所有量词均非否定地出现在公式的最前面，且它的辖域作用于整个公式，则称为此为前束范式（prenexnormalforms）。即前束范式形如(Q1x1)(Q2x2)(Qkxk)B其中Qi(1ik)为或，xi为客体变元。B为不含有量词的公式。,前束范式,12/5/2019,discretemath,前束范式的特点是，所有量词均非否定地出现在公式最前面，且它的辖域一直延伸到公式之末。例如，xyz(P(x,y)Q(y,z)R(x,y)是前束范式。而xP(x)yQ(y)，x(P(x)yQ(x,y)不是前束范式。,前束范式例子,12/5/2019,discretemath,前束范式存在定理：谓词逻辑中任意公式A都有与之等价的前束范式。转化方法：1、把条件或双条件联结词转化。2、利用量词否定等价公式，把否定深入到命题变元和谓词公式的前面。3、换名。4、利用量词作用域的扩张和收缩等价式，把量词提到前面。,量词移前的步骤,12/5/2019,discretemath,前束范式例子,求下面公式的前束范式：(1)xF(x)xG(x)(2)xF(x)xG(x),12/5/2019,discretemath,求解前束范式例子(1),解(1)xF(x)xG(x)xF(x)yG(y)(换名规则)xF(x)yG(y)(量词否定)x(F(x)yG(y)(辖域扩张)xy(F(x)G(y)(辖域扩张)或者xF(x)xG(x)xF(x)xG(x)(量词否定)x(F(x)G(x)(量词分配)由此可知，(1)中公式的前束范式是不唯一的。,12/5/2019,discretemath,求解前束范式例子(2),(2)xF(x)xG(x)xF(x)xG(x)(量词否定)xF(x)yG(y)(换名规则)x(F(x)yG(y)(辖域扩张)xy(F(x)G(y)(辖域扩张)问：(2)的下述求法是否正确？xF(x)xG(x)xF(x)xG(x)x(F(x)G(x)错,12/5/2019,discretemath,12/5/2019,discretemath,例：求以下式的前束范式：（1）xA(x)xB(x)（2）xA(x)xB(x)（3）xy(z(P(x,z)P(y,z)zQ(x,y,z),解（1）xA(x)xB(x)x(A(x)B(x)即为所求前束范式。或xA(x)xB(x)xA(x)xB(x)xA(x)xB(x)x(A(x)B(x)即为所求前束范式。,前束范式例子,12/5/2019,discretemath,或xA(x)xB(x)xA(x)yB(y)x(A(x)yB(y)xy(A(x)B(y)即为所求前束范式。(2)xA(x)xB(x)xA(x)yB(y)(换名)x(A(x)yB(y)xy(A(x)B(y),前束范式例子,12/5/2019,discretemath,(3)xy(z(P(x,z)P(y,z)zQ(x,y,z)xy(z(P(x,z)P(y,z)zQ(x,y,z)xy(z(P(x,z)P(y,z)zQ(x,y,z)xy(z(P(x,z)P(y,z)uQ(x,y,u)xyzu(P(x,z)P(y,z)Q(x,y,u)（或xyzu(P(x,z)P(y,z)Q(x,y,u)）,前束范式例子,12/5/2019,discretemath,1、设个体域D=d1,dn，试用消去量词的方式证明：当A(x)中无自由变元y，B(y)中无自由变元x时，xy(A(x)B(y)yx(A(x)B(y)2、求下列各式的前束范式：（1）xA(x)xB(x)（2）xA(x)xB(x)（3）x(A(x)yB(y)(A(x)中无自由变元y)（4）x(A(x)yB(x,y)(A(x)中无自由变元y)（5）xy(zA(x,y,z)zB(x,y,z),前束范式练习,12/5/2019,discretemath,前束合取范式,定义：一个谓词公式A如果具有如下形式，则称为前束合取范式：(Q1x1)(Q2x2)(Qnxn)(A11A12A1k1)(A21A22A2k2)(Am1Am2Amkm)其中Qi(1in）为或，xi为客体变元，Aij是原子变元或其否定。,12/5/2019,discretemath,前束析取范式,定义：一个谓词公式A如果具有如下形式，则称为前束析取范式：(Q1x1)(Q2x2)(Qnxn)(A11A12A1k1)(A21A22A2k2)(Am1Am2Amkm)其中Qi(1in）为或，xi为客体变元，Aij是原子变元或其否定。,12/5/2019,discretemath,前束范式的的优点是全部量词集中在公式前面，其缺点是各量词的排列无一定规则，这样当把一个公式化归为前束范式时，其表达形式会不唯一。1920年斯柯林(Skolem)提出对前束范式首标中量词出现的次序给出规定：每个存在量词均在全称量词之前。按此规定得到的范式形式，称为斯柯林范式。显然，任一公式均可化为斯柯林范式。优点：全公式按顺序可分为三部分，公式的所有存在量词、所有全称量词和辖域。,斯柯林范式,12/5/2019,discretemath,谓词逻辑的推理理论,谓词逻辑Lp是命题逻辑Ls的进一步深化和发展，因此Ls的推理理论在Lp中几乎可以完全照搬。在Lp中，某些前提和结论可能受到量词的约束，为确立前提和结论之间的内部联系，有必要消去量词和添加量词。正确理解和运用有关量词规则是Lp推理理论中的关键。,12/5/2019,discretemath,谓词演算的推理理论,在谓词逻辑中，如果A1A2AnB是逻辑有效式，则称B是A1,A2,，An的有效结论，记作A1A2AnBAB当且仅当AB是重言式例如：xF(x)xF(x),12/5/2019,discretemath,全称指定规则US，或称为全称量词消去规则,xP(x)P(c)这里P是谓词，而C是论域中某个任意的客体。另一种形式：xA(x)A(y)A(x)对y是自由的,全称指定规则UIuniversalinstantiation,12/5/2019,discretemath,全称推广规则UG，全称量词产生规则,P(x)xP(x)这个规则是要对命题量化，如果能够证明对论域中每一个客体C断言P(c)成立。,全称推广规则UGuniversalgeneralization,12/5/2019,discretemath,存在指定规则ES，或称为存在量词消去规则,xP(x)P(c)C是论域中的某些客体，必须注意，其指定的客体C不是任意的。,存在指定规则EIexistentialinstantiation,12/5/2019,discretemath,存在推广规则EG，存在量词产生规则,P(c)xP(x)这里C是论域中的一个客体，对于某些客体C成立。,存在推广规则EGexistentialgeneralization,12/5/2019,discretemath,12/5/2019,discretemath,试证明下面的苏格拉底论证：所有人都是要死的，苏格拉底是人，因此，苏格拉底是要死的。证明：令M(x):x是人，D(x):x是要死的，s:苏格拉底，原题可符号化为：x(M(x)D(x)，M(s)D(s),苏格拉底论证,12/5/2019,discretemath,推证如下：（1）x(M(x)D(x)前提引入（2）M(s)D(s)UI（1）（3）M(s)前提引入（4）D(s)(2)(3)假言推理,推证苏格拉底论证,12/5/2019,discretemath,谓词推理证明,x(P(x)Q(x)，x(Q(x)R(x)，xR(x)xP(x)证明：xR(x)前提引入R(c)EIx(Q(x)R(x)前提引入Q(c)R(c)UIQ(c)析取三段论x(P(x)Q(x)前提引入P(c)Q(c)UIP(c)拒取式xP(x)EG故，原推证成立，证毕。,12/5/2019,discretemath,谓词推理例子,前提:x(F(x)G(x)，xF(x)结论:xG(x)证明:(1)xF(x)前提引入(2)F(c)EI(1)(3)x(F(x)G(x)前提引入(4)F(c)G(c)UI(3)(5)G(c)(2)(4)假言推理(6)xG(x)EG(5)注意证明过程为：“先EI，后UI”,12/5/2019,discretemath,谓词推理例子,证明:(1)x(F(x)G(x)前提引入(2)F(c)G(c)UI(2)(3)xF(x)前提引入(4)F(c)EI(3)注意：这个证明是错的.(3)(4)应当在(1)(2)之前，(4)中的c是特定的，(2)中的c是任意的。,12/5/2019,discretemath,谓词推理例子,前提:x(F(x)H(x),x(G(x)H(x),结论:x(G(x)F(x)证明:(1)x(F(x)H(x)前提引入(2)x(F(x)H(x)(1)量词否定(3)x(H(x)F(x)(2)靡根律(4)H(y)F(y)UI(3)(5)x(G(x)H(x)前提引入(6)G(y)H(y)UI(5)(7)G(y)F(y)(4)(6)假言三段论(8)x(G(x)F(x)UG(7),12/5/2019,discretemath,EXAMPLE1,Considerthefollowingstatements.Thefirsttwoarecalledpremisesandthethirdiscalledtheconclusion.Theentiresetiscalledanargument.Alllionsarefierce凶猛的.Somelionsdonotdrinkcoffee.Somefiercecreaturesdonotdrinkcoffee.LetP(x),Q(x),andR(x)bethestatementsxisalion,xisfierce,andxdrinkscoffee,respectively.Assumingthattheuniverseofdiscourseisthesetofallcreatures,expressthestatementsintheargumentusingquantifiersandP(x),Q(x),andR(x).,12/5/2019,discretemath,EXAMPLE2,Considerthefollowingstatements,ofwhichthefirstthreearepremisesandthefourthisavalidconclusion.Allhummingbirds蜂鸟arerichlycolored.Nolargebirdsliveonhoney.Birdsthatdonotliveonhoneyaredull晦暗的incolor.Hummingbirdsaresmall.LetP(x),Q(x),R(x),andS(x)bethestatementsxisahummingbird,xislarge,xlivesonhoney,andxisrichlycolored,respectively.Assumingthattheuniverseofdiscourseisthesetofallbirds,expressthestatementsintheargumentusingquantifiersandP(x),Q(x),R(x),andS(x).,12/5/2019,discretemath,小结,1、前束范式2、推理理论推理的形式结构推理正确构造证明新的推理规则全称量词消去规则，记为UI全称量词引入规则，记为UG存在量词消去规则，记为EI存在量词引入规则，记为EG,12/5/2019,discretemath,学习要求,1、深刻理解重要的等值式，并能熟练地使用它们。2、熟练地使用置换规则、换名规则和代替规则。3、准确地求出给定公式的前束范式（形式可不唯一）。4、正确地使用UI、UG、EI、EG规则，特别地要注意它们之间的关系。5、对于给定的推理，正确地构造出它的证明。,12/5/2019,discretemath,练习,P110：31(3)、35(1)、36(3)、37(6),12/5/2019,discretemath,自然推理系统F推理例子,在自然推理系统F中构造下面推理的证明：(1)前提：x(F(x)(G(a)R(x)，xF(x)结论：x(F(x)R(x)(2)前提：x(F(x)G(x)，xG(x)结论：xF(x)(3)前提：x(F(x)G(x)，x(G(x)R(x)，xR(x)结论：xF(x),12/5/2019,discretemath,求解推理例子(1),(1)前提：x(F(x)(G(a)R(x)，xF(x)结论：x(F(x)R(x)证明:xF(x)前提引入F(c)EIx(F(x)(G(a)(R(x)前提引入F(c)(G(a)R(c)UIG(a)R(c)假言推理R(c)化简F(c)R(c)合取x(F(x)R(x)EG,12/5/2019,discretemath,求解推理例子(2),(2)前提：x(F(x)G(x)，xG(x)结论：xF(x)证明：xG(x)前提引入xG(x)置换G(c)UIx(F(x)G(x)前提引入F(c)G(c)UIF(c)析取三段论xF(x)EG,12/5/2019,discretemath,求解推理例子(3),(3)前提：x(F(x)G(x)，x(G(x)R(x)，xR(x)结论：xF(x)证明：x(F(x)G(x)前提引入F(y)G(y)UIx(G(x)R(x)前提引入G(y)R(y)UIxR(x)前提引入R(y)UIG(y)析取三段论F(y)析取三段论xF(x)UG,12/5/2019,discretemath,自然推理系统F推理例子,在自然推理系统F中，证明下面推理：(1)每个有理数都是实数，有的有理数是整数，因此有的实数是整数。(2)有理数、无理数都是实数，虚数不是实数，因此虚数既不是有理数、也不是无理数。(3)不存在能表示成分数的无理数，有理数都能表示成分数，因此有理数都不是无理数。