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

《《前束范式谓词推理》PPT课件.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、谓词公式的标准化形式：前束范式prenexnormalform(PNF)前束合取范式前束析取范式前束范式7/22/2021discretemath在定理的机器证明中，需要消除谓词公式中的量词，因而需要将谓词公式中的量词前束化，即把公式中的量词均提取到公式的前部。即前束范式主要是对量词的位置有要求，而对联接词无要求，这一点与命题逻辑不同。前束范式作用7/22/2021discretemath定义：一个谓词公式，如果它的所有量词均非否定地出现在公式的最前面，且它的辖域作用于整个公式，则称为此为前束范式（prenexnormalf

2、orms）。即前束范式形如(Q1x1)(Q2x2)…(Qkxk)B其中Qi(1≤i≤k)为或，xi为客体变元。B为不含有量词的公式。前束范式7/22/2021discretemath前束范式的特点是，所有量词均非否定地出现在公式最前面，且它的辖域一直延伸到公式之末。例如，xyz((P(x,y)Q(y,z))R(x,y))是前束范式。而xP(x)yQ(y)，x(P(x)yQ(x,y))不是前束范式。前束范式例子7/22/2021discretemath前束范式存在定理：：谓词逻辑中任意公式A都有与

3、之等价的前束范式。转化方法：1、把条件或双条件联结词转化。2、利用量词否定等价公式，把否定深入到命题变元和谓词公式的前面。3、换名。4、利用量词作用域的扩张和收缩等价式，把量词提到前面。量词移前的步骤7/22/2021discretemath前束范式例子求下面公式的前束范式：(1)xF(x)∧┐xG(x)    (2)xF(x)∨┐xG(x)7/22/2021discretemath求解前束范式例子(1)解(1)xF(x)∧┐xG(x)xF(x)∧┐yG(y)(换名规则)xF(x)∧y┐G(y)(

4、量词否定)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))(量词分配)由此可知，(1)中公式的前束范式是不唯一的。7/22/2021discretemath求解前束范式例子(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(y)

5、)(辖域扩张)问：(2)的下述求法是否正确？xF(x)∨┐xG(x)xF(x)∨x┐G(x)x(F(x)∨┐G(x))错7/22/2021discretemath7/22/2021discretemath例：求以下式的前束范式：（1）xA(x)→xB(x)（2）xA(x)∨xB(x)（3）xy(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)x┐A(

6、x)∨xB(x)x(┐A(x)∨B(x))即为所求前束范式。前束范式例子7/22/2021discretemath或xA(x)→xB(x)xA(x)→yB(y)x(A(x)→yB(y))xy(A(x)→B(y))即为所求前束范式。(2)xA(x)∨xB(x)xA(x)∨yB(y)(换名)x(A(x)∨yB(y))xy(A(x)∨B(y))前束范式例子7/22/2021discretemath(3)xy(z(P(x,z)∧P(y,z))→zQ(x,y,z))xy(

7、┐z(P(x,z)∧P(y,z))∨zQ(x,y,z))xy(z(┐P(x,z)∨┐P(y,z))∨zQ(x,y,z))xy(z(┐P(x,z)∨┐P(y,z))∨uQ(x,y,u))xyzu(┐P(x,z)∨┐P(y,z)∨Q(x,y,u))（或xyzu(P(x,z)∧P(y,z)→Q(x,y,u))）前束范式例子7/22/2021discretemath1、设个体域D=d1,…,dn，试用消去量词的方式证明：当A(x)中无自由变元y，B(y)中无自由变元x时，xy(A(

8、x)∧B(y))yx(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）xy(zA