离散数学-05一阶逻辑等值演算与推理(课件模板).ppt

《离散数学-05一阶逻辑等值演算与推理(课件模板).ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第5章一阶逻辑等值演算与推理离散数学大学本科生课程计算机系本章说明本章的主要内容一阶逻辑等值式与基本等值式置换规则、换名规则、代替规则前束范式一阶逻辑推理理论本章与其他各章的关系本章先行基础是前四章本章是集合论各章的先行基础本章主要内容5.1一阶逻辑等值式与置换规则5.2一阶逻辑前束范式5.3一阶逻辑的推理理论5.1一阶逻辑等值式与置换规则在一阶逻辑中，有些命题可以有不同的符号化形式。例如：没有不犯错误的人令M(x):x是人。F(x):x犯错误。则将上述命题的符号化有以下两种正确形式：(1)┐x(M(x)∧┐F(x))(2)x(M(x)→F(x))我们称(1)和(2)是

2、等值的。说明等值式的定义定义5.1设A，B是一阶逻辑中任意两个公式，若AB是永真式，则称A与B是等值的。记做AB，称AB是等值式。例如：判断公式A与B是否等值，等价于判断公式AB是否为永真式。谓词逻辑中关于联结词的等值式与命题逻辑中相关等值式类似。说明一阶逻辑中的一些基本而重要等值式代换实例消去量词等值式量词否定等值式量词辖域收缩与扩张等值式量词分配等值式代换实例由于命题逻辑中的重言式的代换实例都是一阶逻辑中的永真式，因而第二章的16组等值式模式给出的代换实例都是一阶逻辑的等值式的模式。例如：(1)xF(x)┐┐xF(x)（双重否定律）(2)F(x)→G(y

3、)┐F(x)∨G(y)（蕴涵等值式）(3)x(F(x)→G(y))→zH(z)┐x(F(x)→G(y))∨zH(z) （蕴涵等值式）消去量词等值式设个体域为有限集D={a1,a2,…,an},则有（1）xA(x)A(a1)∧A(a2)∧…∧A(an)（2）xA(x)A(a1)∨A(a2)∨…∨A(an)（5.1）量词否定等值式设A(x)是任意的含自由出现个体变项x的公式，则（1）┐xA(x)x┐A(x)（2）┐xA(x)x┐A(x)说明“并不是所有的x都有性质A”与“存在x没有性质A”是一回事。”不存在有性质A的x”与”所有X都没有性质A”是

4、一回事。（5.2）量词辖域收缩与扩张等值式设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)（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.3）（5.4）证明:xA(x)→Bx(A(x)→B)xA(x)→B┐xA(x)∨Bx┐A(x)∨Bx(┐A(x)→B)x(A(

5、x)→B)量词分配等值式设A(x)，B(x)是任意的含自由出现个体变项x的公式，则（1）x(A(x)∧B(x))xA(x)∧xB(x)（2）x(A(x)∨B(x))xA(x)∨xB(x)（5.5）例如，“联欢会上所有人既唱歌又跳舞”和“联欢会上所有人唱歌且所有人跳舞”，这两个语句意义相同。故有(1)式。由(1)式推导(2)式x(A(x)∧B(x))xA(x)∧xB(x)x(┐A(x)∧┐B(x))x┐A(x)∧x┐B(x)┐x(A(x)∨B(x))┐(xA(x)∨xB(x))x(A(x)∨B(x))xA(x)∨xB(x)一阶逻

6、辑等值演算的三条原则置换规则：设Φ(A)是含公式A的公式，Φ(B)是用公式B取代Φ(A)中所有的A之后的公式，若AB，则Φ(A)Φ(B)。换名规则：设A为一公式，将A中某量词辖域中某约束变项的所有出现及相应的指导变元改成该量词辖域中未曾出现过的某个体变项符号，公式的其余部分不变，设所得公式为A'，则A'A。代替规则：设A为一公式，将A中某个自由出现的个体变项的所有出现用A中未曾出现过的个体变项符号代替，A中其余部分不变，设所得公式为A'，则A'A。说明一阶逻辑中的置换规则与命题逻辑中的置换规则形式上完全相同，只是在这里A，B是一阶逻辑公式。例5.1例5.1将下面公式

7、化成与之等值的公式，使其没有既是约束出现又是自由出现的个体变项。(1)xF(x,y,z)→yG(x,y,z)(2)x(F(x,y)→yG(x,y,z))(1)xF(x,y,z)→yG(x,y,z)tF(t,y,z)→yG(x,y,z)(换名规则)tF(t,y,z)→wG(x,w,z)(换名规则)或xF(x,y,z)→yG(x,y,z)xF(x,t,z)→yG(x,y,z)(代替规则)xF(x,t,z)→yG(w,y,z)(代替规则)解答例5.1的解答(2)x(F(x,y)→