&amp#167;4 谓词演算的性质.ppt

《&amp#167;4 谓词演算的性质.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、在命题演算中，代换定理是基于同态映射:P1→P2，这里P1,P2为二个命题代数，如果P1,P2为谓词代数，则根据同态映射的要求，P1,P2应该有相同的运算集，对其个体符集有新的要求定义21.17:设P1=P(Y1)和P2=P(Y2)，其个体变元与个体常元分别为X1,C1和X2,C2，并且或者C1=或者C2。一个半同态映射(,):(P1,X1∪C1)→(P2,X2∪C2)是一对映射:P1→P2;:X1∪C1→X2∪C2，它们联合实现了映射p(x,c)→(p)((x),(c)),且具有性质：(1)(X1)X2，(C1)C2，而且在X1

2、上是一对一的。(2)是{F,→}-同态映射。(3)对任何pP1有(xp)=(x)(p)。引理21.3:设(,):(P1,X1∪C1)→(P2,X2∪C2)是半同态映射，pP1，并且假设xvar(p)。则(x)var((p))。证明:xvar(p),(1)x不在p中出现(2)x在p中约束出现都要利用在X1上是一对一的定理21.9(代换定理)设(,):(P1,X1∪C1)→(P2,X2∪C2)是半同态映射，AP1,pP1。如果A┣p，则(A)┣(p)。证明:对证明序列用归纳法n=1,p1=pAP1∪A对n>1,假设对一切证

3、明序列

4、式。定义21.19(斯柯伦范式):pP(Y)是前束范式而且它的形式：p=1x12x2…kxkq中的所有全称量词(如果有的话)总在存在量词(如果有的话)的后面，则称p为斯柯伦(T.Skolem)范式。§4谓词演算的性质谓词逻辑Pred(Y)。是Y上的关于类型{F,→,x

5、xX}的自由代数赋值形式证明赋值解释和证明之间的关系作业：P42520,21,23,31(7)

6、-(pq)→q证明:即证

7、-¬(¬¬p→¬q)→q由演绎定理即证{¬(¬¬p→¬q)}

8、-qp1=¬(¬¬p→¬q)=(¬¬p→(q→F))→F(A)p2=((¬¬p→(q→F))→F

9、)→((q→F)→((¬¬p→(q→F))→F))(A1)p3=(q→F)→((¬¬p→(q→F))→F)(p1,p2MP)P4=((q→F)→((¬¬p→(q→F))→F))→((((q→F)→(¬¬p→(q→F)))→((q→F)→F)))(A2)p5=((q→F)→(¬¬p→(q→F)))→((q→F)→F)(p3,p4MP)p6=(q→F)→(¬¬p→(q→F))(A1)p7=(q→F)→F=¬¬q(p6,p5MP)P8=¬¬q→q(A3)P9=q(p7,p8MP)可简单，利用¬q→(¬¬p→¬q)p1=¬q→(¬¬p→¬q)A1.P2=(¬q→(¬¬p

10、→¬q))→(¬(¬¬p→¬q)→¬¬q)已证P3=¬(¬¬p→¬q)→¬¬qp1,p2MPP4=¬(¬¬p→¬q)AP5=¬¬qp4,p3MPP6=¬¬q→q(A3)P7=qp5,p6MPP4231,2,6,7,8