离散数学---一阶逻辑的等值式.ppt

《离散数学---一阶逻辑的等值式.ppt》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、2.3一阶逻辑的等值式设A和B是一阶逻辑中任意的两个公式，若AB是永真式，则称A与B等值，记为AB，称AB为等值式。由于命题逻辑中的永真式的替换实例是永真式，因此在命题逻辑中给出的等值式的替换实例都是一阶逻辑的等值式。一阶逻辑中的等值式1）在有限个体域D={a1,a2,…,an}中消除量词：(1).xA(x)A(a1)A(a2)…A(an)(2).xA(x)A(a1)A(a2)…A(an)2）量词否定等值式：(1).(xA(x))x(A(x))(2).(xA(x))x(A(x))一阶逻辑中的等值式（续）3）量词辖域的收缩与扩

2、张等值式：下述等值式中，变元x不在B中出现(1).x(A(x)B)(xA(x))B(2).x(A(x)B)(xA(x))B(3).x(A(x)B)(xA(x))B(4).x(BA(x))B(xA(x))(5).x(A(x)B)(xA(x))B(6).x(A(x)B)(xA(x))B(7).x(A(x)B)(xA(x))B(8).x(BA(x))B(xA(x))一阶逻辑中的等值式（续）4）量词分配等值式：(1).x(A(x)B(x))(xA(x))(xB(x))(2).x(A(x

3、)B(x))(xA(x))(xB(x))5）量词顺序变换等值式：(1).xy(A(x,y))yx(A(x,y))(2).xy(A(x,y))yx(A(x,y))前束范式设A为一阶逻辑公式，若A具有如下形式：Q1x1Q2x2…QnxnB则称A为前束范式(prenexnormalform)。其中Qi(1in)是或，B为不含量词的公式。对于任意的一阶逻辑公式A，都存在与之等值的前束范式。如何求公式的前束范式求一个公式的前束范式，无非是通过等值式将其所有的量词移到整个公式的前面。根据一阶逻辑公式的归纳定义，可将公式的形式分为以下几种：(i)

4、.量词与否定：(xA(x))、(xA(x))(ii).量词与析取：xA(x)yB(y)、xA(x)yB(y)、xA(x)yB(y)、xA(x)yB(y)(iii).量词与合取：xA(x)yB(y)、xA(x)yB(y)、xA(x)yB(y)、xA(x)yB(y)(iv).量词与蕴涵：xA(x)yB(y)、xA(x)yB(y)、xA(x)yB(y)、xA(x)yB(y)(v).量词与等价：xA(x)yB(y)、xA(x)yB(y)、xA(x)yB(y)、xA(x)yB(

5、y)对于公式xA(x)yB(y)和xA(x)yB(y)对于公式xA(x)yB(y)，由于对合取有分配律，所以可变换为：xA(x)yB(y)xA(x)xB(x)x(A(x)B(x))注意运用此变换的前提是B(y)中不出现x，如果B(y)中出现x，则可使用换名规则（如果x是约束出现）或者是替换规则（如果x是自由出现）先将x变为其他变换符号。对于公式xA(x)yB(y)，由于对合取没有分配律，所以只能变换为：xA(x)yB(y)xy(A(x)B(y))显然对于公式xA(x)yB(y)、xA(x)yB(y

6、)都只能变换为：xA(x)yB(y)xy(A(x)B(y))、xA(x)yB(y)xy(A(x)B(y))对于公式xA(x)yB(y)和xA(x)yB(y)对于公式xA(x)yB(y)，由于对析取有分配律，所以可变换为：xA(x)yB(y)xA(x)xB(x)x(A(x)B(x))注意运用此变换的前提是B(y)中不出现x，如果B(y)中出现x，则可使用换名规则（如果x是约束出现）或者是替换规则（如果x是自由出现）先将x变为其他变换符号。对于公式xA(x)yB(y)，由于对析取没有分配律，所以只能

7、变换为：xA(x)yB(y)xy(A(x)B(y))显然对于公式xA(x)yB(y)、xA(x)yB(y)都只能变换为：xA(x)yB(y)xy(A(x)B(y))、xA(x)yB(y)xy(A(x)B(y))求前束范式例1求下列公式的前束范式：1、xA(x)∧xB(x)2、xA(x)∨xB(x)3、xA(x)∨xB(x)4、xA(x)∧xB(x)1、x(A(x)∧B(x))2、x(A(x)∨B(x))3、xA(x)∨yB(y)xy(A(x)∨B(y