F5一阶逻辑等值演算与推理

091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则§5.1一阶逻辑等值式与置换规则§5.2一阶逻辑的前束范式第五章一阶逻辑等值演算和推理§5.3一阶逻辑的推理理论091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则引例2令F(x):x是人;G(x):x有横财,H(x):x是富的.“人无横财不富”可符号化为________.(A)x(F(x)(G(x)H(x))),(B)x((F(x)G(x))H(x)),(C)x((F(x)H(x))G(x)),(D)x((G(x)H(x))G(x)),(E)x(F(x)G(x)H(x)),引例1令H(x):x是人;M(x):x是要死的.“人都是要死的”:x(H(x)M(x)),⑴“没有人是不死的”:x(H(x)M(x)).⑵091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则logicallyequivalenct,calculusoffirstorderlogic若AB是永真式,则称公式A与B是等值的:AB.†判断A与B是否等值,即判断AB是否永真,根据永真式的定义来判断一般比较困难,但可以运用一阶逻辑的等值演算:利用已知的等值式,根据规则,推演出其它的等值式.091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则/substitutioninstance第一组代换实例命题逻辑中的重言式的代换实例都是一阶逻辑中的永真式,因而命题逻辑中的等值式†给出的代换实例都是一阶逻辑的等值式.例如AA的代换实例:xF(x)xF(x)xy(F(x,y)G(x,y))xy(F(x,y)G(x,y))又如ABAB的代换实例:F(x)G(y)F(x)G(y),x(F(x)G(y))zH(z)x(F(x)G(y))zH(z))基本等值式091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则/quantifierelimination第二组1.消去量词等值式设个体域为有限域D={a1,a2,…,an},则有(1)xA(x)A(a1)A(a2)…A(an)(2)xA(x)A(a1)A(a2)…A(an)(5.1)2.量词否定等值式(1)xA(x)xA(x)(2)xA(x)xA(x)(5.2)基本等值式091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则基本等值式3.量词辖域收缩与扩张等值式设A(x)含x的自由出现,而B不含x的自由出现,则(1)x(A(x)B)xA(x)Bx(A(x)B)xA(x)Bx(A(x)B)xA(x)Bx(BA(x))BxA(x)(5.3)(2)x(A(x)B)xA(x)Bx(A(x)B)xA(x)Bx(A(x)B)xA(x)Bx(BA(x))BxA(x)(5.4)注意:A(x),B含或不含x.091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则†量词对蕴含分配的时候前件中的量词要改变:x(A(x)B)xA(x)Bx(A(x)B)xA(x)B证明x(A(x)B)x(A(x)B)xA(x)xBxA(x)xB(xA(x)xB).4.量词分配等值式(1)x(A(x)B(x))xA(x)xB(x)(2)x(A(x)B(x))xA(x)xB(x)(5.5)/quantifierdistribution091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则基本规则/replacement等值演算有三条规则.1.置换规则(A)是含公式A的公式,若AB,则(A)(B).2.换名规则将公式A中某量词辖域中的约束变元及其指导变元改成该辖域中未曾出现过的个体变元,设所得公式为A',则A'A.例如A(x)=xF(x)yG(x,y)可换名为A'(x)=zF(z)yG(x,y),或A''(x)=xF(x)zG(x,z),或A'''(x)=yF(y)yG(x,y).但A(x)不可改为B=xF(x)xG(x,x),/variablerenaming091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则基本规则/replacement3.代替规则将公式A中某个自由变项用A中未曾出现过的个体变项符号代替,设所得公式为A',则A'A.例如A(x,y)=uF(u)vG(x,y,v)可代替为A'(z,y)=uF(u)vG(z,y,v).但A(x,y)不可代替为B(y)=A''(y,y)=uF(u)vG(y,y,v).091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则例1求下面公式的等值式,使约束变项与自由变项符号不同.(1)A=xF(x,y,z)yG(x,y,z);(2)B=x(F(x,y)yG(x,y,z))解(1)A=xF(x,y,z)yG(x,y,z)tF(t,y,z)yG(x,y,z)(换名规则)tF(t,y,z)wG(x,w,z)(换名规则)或A=xF(x,y,z)yG(x,y,z)xF(x,t,z)yG(x,y,z)(代替规则)xF(x,t,z)yG(w,y,z)(代替规则).091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则(2)B=x(F(x,y)yG(x,y,z))B=x(F(x,y)yG(x,y,z))x(F(x,t)yG(x,y,z))(代替规则)或者B=x(F(x,y)yG(x,y,z))x(F(x,y)tG(x,t,z))(换名规则)091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则例2说明对无分配律,而对无分配律.(1)x(A(x)B(x))xA(x)xB(x);(2)x(A(x)B(x))xA(x)xB(x),其中A(x),B(x)含自由变元x.证只要证明在某个解释下两边的式子不等值.取个体域,解释为(1)LHS:自然数或者是奇数或者是偶数,RHS:自然数都是奇数或自然数都是偶数.(2)LHS:有一个自然数既是奇数也是偶数,RHS:有一个奇自然数且有一个偶自然数.091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则例3设个体域为D={a,b,c},消去公式中的量词:(1)x(F(x)G(x));(2)x(F(x)yG(y));(3)xyF(x,y).解(1)x(F(x)G(x))(F(a)G(a))(F(b)G(b))(F(c)G(c))(2)x(F(x)yG(y))xF(x)yG(y)(分配律)(F(a)F(b)F(c))(G(a)G(b)G(c))如果不将量词的辖域缩小,演算过程较长.注意,此处yG(y)是与x无关.091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则(3)xyF(x,y)x(F(x,a)F(x,b)F(x,c))(F(a,a)F(a,b)F(a,c))(F(b,a)F(b,b)F(b,c))(F(c,a)F(c,b)F(c,c)).†或者先消去存在量词:xyF(x,y)yF(a,y)yF(b,y)yF(c,y)(F(a,a)F(a,b)F(a,c))(F(b,a)F(b,b)F(b,c))(F(c,a)F(c,b)F(c,c)).091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则例5证明下列等值式.(1)x(M(x)F(x))x(M(x)F(x));(2)x(F(x)G(x))x(F(x)G(x));(3)xy(F(x)G(y)H(x,y))xy(F(x)G(y)H(x,y));(4)xy(F(x)G(y)L(x,y))xy(F(x)G(y)L(x,y))证(1)x(M(x)F(x))x(M(x)F(x))(量词否定)x(M(x)F(x))(置换规则)x(M(x)F(x))(置换规则).091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则(2)x(F(x)G(x))x(F(x)G(x));x(F(x)G(x))x(F(x)G(x))(量词否定)x(F(x)G(x))(置换规则)x(F(x)G(x))(置换规则).(3)xy(F(x)G(y)H(x,y))xy(F(x)G(y)H(x,y));xy(F(x)G(y)H(x,y))x(y((F(x)G(y))H(x,y)))xy((F(x)G(y))H(x,y))xy(F(x)G(y)H(x,y)).091离散数学(60).W&M.§5.1一阶逻辑等值式与置换规则(4)xy(F(x)G(y)L(x,y))xy(F(x)G(y)L(x,y)).xy(F(x)G(y)L(x,y))xy(F(x)G(y)L(x,y))xy(F(x)G(y)L(x,y))xy((F(x)G(y))L(x,y))xy(F(x)G(y)L(x,y)).091离散数学(60).W&M.§5.2一阶逻辑的前束范式§5.1一阶逻辑等值式与置换规则§5.2一阶逻辑的前束范式第五章一阶逻辑等值演算和推理§5.3一阶逻辑的推理理论091离散数学(60).W&M.§5.2一阶逻辑的前束范式前束范式?xy(F(x)G(y)H(x,y))xyz(F(x)G(y)H(z)L(x,y,z))x(F(x)y(G(y)H(x,y)))x(F(x)y(G(y)H(x,y)))形如Q1x1Q2x2…QkxkB的公式叫作前束范式,其中Qi为或,而B中不含量词.定理5.1(前束范式存在定理)一阶逻辑中的任何公式都存在与之等值的前束范式.一阶逻辑推理中要把公式转换成前束范式,即把各量词移到公式的最前端,使其辖域最大化.091离散数学(60).W&M.§5.2一阶逻辑的前束范式例6求前束范式:(1)xF(x)xG(x);(2)xF(x)xG(x).解(1)xF(x)xG(x)xF(x)yG(y)(换名规则)xF(x)yG(y)(量词否定)x(F(x)yG(y))(辖域扩张)xy(F(x)G(y))(辖域扩张)或者xF(x)xG(x)xF(x)xG(x)(量词否定)x(F(x)G(x))(对分配)可见前束范式是不唯一的.091离散数学(60).W&M.§5.2一阶逻辑的前束范式(2)xF(x)xG(x)xF(x)xG(x)(量词否定)xF(x)yG(y)(换名规则)x(F(x)yG(y))(辖域扩张)xy(F(x)G(x))(辖域扩张).091离散数学(60).W&M.§5.2一阶逻辑的前束范式例7求下列各公式的前束范式:(1)xF(x,y)yG(x,y),(2)(x1F(x1,x2)x2G(x2))x1H(x1,x2,x3).解(1)xF(