1、第五章 一阶逻辑等值演算与推理,1,本章主要内容,5.1一阶逻辑等值式与置换规则5.2一阶逻辑前束范式5.3一阶逻辑的推理理论,2,5.1一阶逻辑等值式与置换规则,等值式的概念基本等值式等值演算与置换规则,3,所有的学生都上课了，这是错的。,令 F(x): x是学生, G(x): x上课了。,这句话相当于“有些学生没有上课”。,4,一、等值式的概念,定义：若AB为永真式，则称A与B是等值的，记作 AB，并称AB为等值式。其中A、B是一阶逻辑中任意的两个合式公式。,5,二、基本等值式,命题逻辑中16组基本等值式的代换实例,例：xF(x)yG(y) xF(x)yG(y) (xF(x)yG(y) x
2、F(x)yG(y),即命题逻辑中的基本等值式在谓词逻辑中均适用。,6,二、基本等值式,有限个体域中，消去量词等值式,设个体域为D=a1,a2,an xA(x) A(a1)A(a2)A(an) xA(x) A(a1)A(a2)A(an),7,二、基本等值式,量词否定等值式,“并不是所有的人都是黄皮肤。”,这句话相当于“有的人不是黄皮肤。”,8,二、基本等值式,量词辖域收缩与扩张等值式,设A(x)是含x自由出现的公式，B中不含x的出现。,关于全称量词： x(A(x)B)xA(x)B x(A(x)B)xA(x)B x(A(x)B)xA(x)B x(BA(x)BxA(x),9,二、基本等值式,关于存在
3、量词: x(A(x)B)xA(x)B x(A(x)B)xA(x)B x(A(x)B)xA(x)B x(BA(x)BxA(x),10,二、基本等值式,量词分配等值式,x(A(x)B(x)xA(x)xB(x)x(A(x)B(x)xA(x)xB(x),注意：对无分配律，对无分配律,11,三、等值演算与置换规则,置换规则：设(A)是含有公式A的公式，用公式B置换(A)中所有的A后得到新的公式(B)，若AB, 则(B)(A),等值演算的基础：（1）一阶逻辑的基本等值式；（2）置换规则、换名规则、代替规则。,12,例题,例1：下面的命题都有两种不同的符号化形式，写出其中的一种，然后通过等值演算得到另一种。
4、 (1) 没有不犯错误的人 (2) 不是所有的人都爱看电影,13,(1) 没有不犯错误的人,令F(x)：x是人，G(x)：x犯错误,例题,14,(2) 不是所有的人都爱看电影,令F(x)：x是人，G(x)：爱看电影,例题,15,例2：设个体域D=a,b,c，在D中消去下列公式中的量词。,两次使用“消去等值式”,例题,16,量词辖域收缩与扩张等值式,解法二：,小结：采用不同的演算过程同样可以达到消去量词的目的，但是如何演算才更简单呢？结论是将量词辖域尽可能的缩小，然后再消量词。,例题,17,方法2：,例题,18,(3)当个体域D=a,b,提问：如果先消去全称量词，后消去存在量词，结果会怎样？,例
5、题,19,该题量词的辖域已经不能再缩小了，所以演算过程无法再简化，演算结果也不易化的更简单。,两种消去顺序得到的结果相同。,例题,20,例题,21,在 I 下求下列各式的真值。,例题,22,计算过程见教材,例题,23,例4：证明下面的谓词公式是永真式。,证明谓词公式是永真式不能像命题公式那样使用真值表。常用的方法是等值演算。,例题,24,经过等值演算可知该公式是永真式。,例题,25,例题,26,兔子比乌龟跑得快。,令：F(x):x是兔子 G(y):y是乌龟 L(x,y):x比y跑得快,命题符号化为：,另外一种等值的符号化形式为：,27,5.2 前束范式,定义：设A为一个一阶逻辑公式, 若A具有
6、如下形式Q1x1Q2x2QkxkB, 则称A为前束范式, 其中Qi (1ik)为或，B为不含量词的公式。,例：xy(F(x)(G(y)H(x,y) x(F(x)G(x),x(F(x)G(x)不是前束范式。,B,前束范式,B,28,5.2 前束范式,(1) x(M(x)F(x)解： x(M(x)F(x) x(M(x)F(x) （量词否定等值式） x(M(x)F(x),两步结果都是原公式的前束范式。,例1：求下列公式的前束范式,29,5.2 前束范式,(2) xF(x)xG(x)解： xF(x)xG(x) xF(x)xG(x) （量词否定等值式） x(F(x)G(x) （量词分配等值式）,另有一种
7、形式如下：,30,5.2 前束范式,xF(x)xG(x) xF(x)xG(x) xF(x)yG(y) ( 换名规则 ) x(F(x)yG(y) ) ( 量词辖域扩张 ) xy(F(x)G(y) ( 量词辖域扩张 ),31,5.2 前束范式,(3) xF(x)xG(x) 解 xF(x)xG(x) xF(x)xG(x) x(F(x)G(x) 或 xy(F(x)G(y),32,5.2 前束范式,(4) xF(x)y(G(x,y)H(y) 解 xF(x)y(G(x,y)H(y) zF(z)y(G(x,y)H(y) (换名规则) zy(F(z)(G(x,y)H(y)或 xF(x)y(G(t,y)H(y)
8、 (代替规则) xy (F(x)(G(t,y)H(y),33,5.2 前束范式,(5) x(F(x,y)y(G(x,y)H(x,z)解：既可用换名规则, 也可用代替规则 x(F(x,y)y(G(x,y)H(x,z) x(F(x,u)y(G(x,y)H(x,z) xy(F(x,u)G(x,y)H(x,z)注意：x与y不能颠倒,(换名规则),34,5.2 前束范式,（6）,35,5.2 前束范式,例题小结：公式的前束范式不惟一；求公式的前束范式的方法: 利用基本等值式、置换规则、换名规则、代替规则进行等值演算。,定理：一阶逻辑中的任何公式都存在与之等值的前束范式。,36,5.3一阶逻辑的推理理论,
9、推理的形式结构重要的推理定律推理规则构造证明（附加前提证明法）,37,一、推理的形式结构,推理的形式结构有两种： 第一种 A1A2AkB (*) 第二种 前提：A1，A2，Ak 结论： B 其中 A1,A2,Ak,B为一阶逻辑公式. 若(*)为永真式, 则称推理正确, 否则称推理不正确,38,一、推理的形式结构,判断推理是否正确的方法：等值演算法，应用这种方法时采用第一种形式结构；构造证明法，采用第二种形式结构。,39,二、重要的推理定律,第一组 命题逻辑推理定律代换实例 如：xF(x)yG(y)xF(x) 化简律代换实例.,第二组 由基本等值式生成的推理定律,如：由 xA(x)xA(x) 生
10、成 xA(x)xA(x), xA(x)xA(x), ,40,二、重要的推理定律,第三组 xA(x)xB(x)x(A(x)B(x) x(A(x)B(x)xA(x)xB(x),41,三、推理规则,(1)前提引入规则 (2)结论引入规则(3)置换规则 (4)假言推理规则(5)附加规则 (6)化简规则(7)拒取式规则 (8)假言三段论规则(9)析取三段论规则 (10)构造性二难推理规则(11)合取引入规则,42,(12) 全称量词消去规则（记为UI）,注意：下面的规则只能用于前束范式。,在(1)式中，y应为任意的不在A(x)中约束出现的个体变项。在第二式中，c为任意的未在A(x)中出现过的个体常项。用
11、y或c去取代A(x)中的自由出现的x时，一定要在x自由出现的一切地方进行取代。,43,(13) 全称量词引入规则（记为UG）,无论A(y)中自由出现的个体变项y取何值，A(y)应该均为真。 x不约束出现在A(y)中。,若对A(y) 应用UG规则时，用在A(y) 中约束出现的x代替y，则得到,44,(14) 存在量词消去规则（记为EI）,c是个体域中使A为真的某个确定的个体，且c不在A(x)中出现。若A(x)中除自由出现的x外，还有其他自由出现的个体变项，此规则不能使用。,对公式 能否用EI规则？,提问：,45,三、推理规则,前提引入,(1)UI规则,(2)EI规则,(3)UG规则,46,(15
12、) 存在量词引入规则（记为EG）,该式成立的条件是：c是使A为真的特定个体常项.取代c的x不能在A(c)中出现过.,47,四、构造推理证明,一阶逻辑自然推理系统F1.字母表，即一阶语言的字母表。2.合式公式。3.推理规则,构造推理证明的方法：直接法，附加前提引入法和归谬法。,48,四、构造推理证明,例1：在自然推理系统中，指出下面各证明序列中的错误。,49,四、构造推理证明,50,四、构造推理证明,例2： 证明苏格拉底三段论: “人都是要死的, 苏格拉底是人，所以苏格拉底是要死的。”,令：F(x): x是人, G(x): x是要死的, a: 苏格拉底 前提：x(F(x)G(x)，F(a) 结论
13、：G(a),51,四、构造推理证明,证明： F(a) 前提引入 x(F(x)G(x) 前提引入 F(a)G(a) UI G(a) 假言推理注意：使用UI时，用a取代x。,52,四、构造推理证明,例3：乌鸦都不是白色的。 北京鸭是白色的。 因此，北京鸭不是乌鸦。,令：F(x): x是乌鸦, G(x): x是北京鸭, H(x): x是白色的 前提：x(F(x)H(x)， x(G(x)H(x) 结论：x(G(x)F(x),53,四、构造推理证明,证明： x(F(x)H(x) 前提引入 F(y)H(y) UI x(G(x)H(x) 前提引入 G(y)H(y) UI H(y)F(y) 置换 G(y)F(
14、y) 假言三段论 x(G(x)F(x) UG,54,四、构造推理证明,例4：构造下述推理证明 前提：x(F(x)G(x)，xF(x) 结论：xG(x),证明： xF(x) 前提引入 x(F(x)G(x) 前提引入,55,四、构造推理证明, F(c) EI F(c)G(c) UI G(c) 假言推理 xG(x) EG,56,四、构造推理证明,例5： 构造下述推理证明 前提：xF(x)xG(x) 结论：x(F(x)G(x),证明： xF(x)xG(x) 前提引入 xy(F(x)G(y) 置换 x(F(x)G(z) UI,57,四、构造推理证明, F(z)G(z) UI x(F(x)G(x) UG
15、说明: 不能对xF(x)xG(x)消量词, 因为它不是前束范式。对此题不能用附加前提证明法。,58,四、构造推理证明,例6：构造下述推理证明 前提：x(F(x)G(x) 结论：xF(x)xG(x),59,四、构造推理证明,证明： xF(x) 附加前提引入 F(y) UI x(F(x)G(x) 前提引入 F(y)G(y) UI G(y) 假言推理 xG(x) UG,60,四、构造推理证明,例7：构造下述推理证明前提： x(F(x)G(x) ， x(F(x)H(x)结论： x(G(x)H(x),证明： x(F(x)H(x) 前提引入 F(c)H(c) EI,61,四、构造推理证明, F(c) 化简 H(c) 化简 x(F(x)G(x) 前提引入 F(c)G(c) UI G(c) 假言推理 G(c)H(c) 合取 x(G(x)H(x) EG,62,
