一阶逻辑等值演算与推理.ppt

第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)是等值的。,说明,等值式的定义,定义5.1 设A，B是一阶逻辑中任意两个公式，若 AB是永真式，则称A与B是等值的。记做AB，称 AB 是等值式。,例如：,判断公式A与B是否等值，等价于判断公式AB是否为永真式。谓词逻辑中关于联结词的等值式与命题逻辑中相关等值式类似。,说明,一阶逻辑中的一些基本而重要等值式,代换实例消去量词等值式 量词否定等值式 量词辖域收缩与扩张等值式 量词分配等值式,代换实例,由于命题逻辑中的重言式的代换实例都是一阶逻辑中的永真式，因而第二章的16组等值式模式给出的代换实例都是一阶逻辑的等值式的模式。例如：(1)xF(x)xF(x)（双重否定律）(2)F(x)G(y)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)xA(x)（2）xA(x)xA(x),说明,“并不是所有的x都有性质A”与“存在x没有性质A”是一回事。”不存在有性质A的x”与”所有X都没有性质A”是一回事。,（5.2）,量词辖域收缩与扩张等值式,设A(x)是任意的含自由出现个体变项x的公式，B中不含x的出现，则（1）x(A(x)B)xA(x)Bx(A(x)B)xA(x)Bx(A(x)B)xA(x)Bx(BA(x)BxA(x)（2）x(A(x)B)xA(x)Bx(A(x)B)xA(x)Bx(A(x)B)xA(x)Bx(BA(x)BxA(x),（5.3）,（5.4）,证明:xA(x)B x(A(x)B),xA(x)B xA(x)B xA(x)B x(A(x)B)x(A(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)xA(x)xB(x)x(A(x)B(x)(xA(x)xB(x)x(A(x)B(x)xA(x)xB(x),一阶逻辑等值演算的三条原则,置换规则：设(A)是含公式A的公式，(B)是用公式B取代(A)中所有的A之后的公式，若AB，则(A)(B)。换名规则：设A为一公式，将A中某量词辖域中某约束变项的所有出现及相应的指导变元改成该量词辖域中未曾出现过的某个体变项符号，公式的其余部分不变，设所得公式为A，则AA。代替规则：设A为一公式，将A中某个自由出现的个体变项的所有出现用A中未曾出现过的个体变项符号代替，A中其余部分不变，设所得公式为A，则AA。,说明,一阶逻辑中的置换规则与命题逻辑中的置换规则形式上完全相同，只是在这里A，B是一阶逻辑公式。,例5.1,例5.1 将下面公式化成与之等值的公式，使其没有既是约束出现又是自由出现的个体变项。(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)yG(x,y,z),x(F(x,t)yG(x,y,z),(代替规则),或x(F(x,y)yG(x,y,z),x(F(x,y)tG(x,t,z),(换名规则),解答,换名规则和代替规则的关系,换名规则和代替规则之间的共同点都是不能改变原有的约束关系，而不同点是：（1）施行的对象不同：换名规则是对约束变元施行，代替规则是对自由变元施行；（2）施行的范围不同：换名规则可以只对公式中的一个量词及其辖域内施行，即只对公式的一个子公式施行；而代替规则必须对整个公式同一个自由变元的所有自由出现同时施行，即必须对整个公式施行；,换名规则和代替规则的关系（续）,（3）施行后的结果不同：换名后，公式含义不变，因为约束变元只改名为另一个个体变元，约束关系不改变，约束变元不能改名为个体常量；代替后，不仅可用另一个个体变元进行代入，并且也可用个体常量去代入，从而使公式由具有普遍意义变为仅对该个体常量有意义，即公式的含义改变了。,例5.2,例5.2 证明（1）x(A(x)B(x)xA(x)xB(x)（2）x(A(x)B(x)xA(x)xB(x)其中A(x)，B(x)为含x自由出现的公式。,只要证明在某个解释下两边的式子不等值。取解释I：个体域为自然数集合N；(1)取F(x)：x是奇数，代替A(x)；取G(x)：x是偶数，代替B(x)。则x(F(x)G(x)为真命题，而xF(x)xG(x)为假命题。两边不等值。,证明,例5.2,(2)x(A(x)B(x)xA(x)xB(x)x(F(x)G(x)：有些x既是奇数又是偶数为假命题；而xF(x)xG(x)：有些x是奇数并且有些x是偶数为真命题。两边不等值。,证明,说明,全称量词“”对“”无分配律。存在量词“”对“”无分配律。当B(x)换成没有x出现的B时，则有 x(A(x)B)xA(x)B x(A(x)B)xA(x)B,例5.3消去量词,例5.3 设个体域为Da,b,c，将下面各公式的量词消去：(1)x(F(x)G(x)(2)x(F(x)yG(y)(3)xyF(x,y),说明,如果不用公式(5.3)将量词的辖域缩小，演算过程较长。注意，此时yG(y)是与x无关的公式B。,解答,(1)x(F(x)G(x)(F(a)G(a)(F(b)G(b)(F(c)G(c)(2)x(F(x)yG(y)xF(x)yG(y)(公式5.3)(F(a)F(b)F(c)(G(a)G(b)G(c),例5.3消去量词,(3)xyF(x,y)x(F(x,a)F(x,b)F(x,c)(F(a,a)F(a,b)F(a,c)(F(b,a)F(b,b)F(b,c)(F(c,a)F(c,b)F(c,c)在演算中先消去存在量词也可以，得到结果是等值的。xyF(x,y)yF(a,y)yF(b,y)yF(c,y)(F(a,a)F(a,b)F(a,c)(F(b,a)F(b,b)F(b,c)(F(c,a)F(c,b)F(c,c),例5.4,例5.4 给定解释I如下：（a）个体域 D2,3（b）D中特定元素（c）D上的特定函数(x)为：（d）D的特定谓词,在解释I下求下列各式的值：（1）x(F(x)G(x,a)（2）x(F(f(x)G(x,f(x)（3）xyL(x,y)（4）yxL(x,y),例5.4的解答,（1）x(F(x)G(x,a)(F(2)G(2,2)(F(3)G(3,2)(01)(11)0（2）x(F(f(x)G(x,f(x)(F(f(2)G(2,f(2)(F(f(3)G(3,f(3)(F(3)G(2,3)(F(2)G(3,2)(11)(01)1,例5.4的解答,（3）xyL(x,y)(L(2,2)L(2,3)(L(3,2)L(3,3)(10)(01)1（4）yxL(x,y)y(L(2,y)L(3,y)(L(2,2)L(3,2)(L(2,3)L(3,3)(10)(01)0,说明,由(3)，(4)的结果进一步可以说明量词的次序不能随意颠倒。,例5.5,例5.5 证明下列等值式。（1）x(M(x)F(x)x(M(x)F(x)（2）x(F(x)G(x)x(F(x)G(x)（3）xy(F(x)G(y)H(x，y)xy(F(x)G(y)H(x,y)（4）xy(F(x)G(y)L(x，y)xy(F(x)G(y)L(x,y),例5.5的证明,（1）x(M(x)F(x)x(M(x)F(x)x(M(x)F(x)x(M(x)F(x)x(M(x)F(x)x(M(x)F(x)（2）x(F(x)G(x)x(F(x)G(x)x(F(x)G(x)x(F(x)G(x)x(F(x)G(x)x(F(x)G(x),例5.5的证明,（3）xy(F(x)G(y)H(x，y)xy(F(x)G(y)H(x,y)xy(F(x)G(y)H(x，y)x(y(F(x)G(y)H(x，y)xy(F(x)G(y)H(x，y)xy(F(x)G(y)H(x,y),例5.5的证明,（4）xy(F(x)G(y)L(x，y)xy(F(x)G(y)L(x,y)xy(F(x)G(y)L(x，y)x(y(F(x)G(y)L(x，y)xy(F(x)G(y)L(x，y)xy(F(x)G(y)L(x,y)xy(F(x)G(y)L(x,y),5.2 一阶逻辑前束范式,定义5.2 设A为一个一阶逻辑公式，若A具有如下形式Q1x1Q2x2 QkxkB则称A为前束范式，其中Qi(1ik)为或，B为不含量词的公式。前束范式的例子：xy(F(x)G(y)H(x，y)xyz(F(x)G(y)H(z)L(x，y，z)不是前束范式的例子：x(F(x)y(G(y)H(x，y)x(F(x)y(G(y)H(x，y),前束范式存在定理,定理5.1 一阶逻辑中的任何公式都存在与之等值的前束范式。,说明,求前束范式的过程，就是制造量词辖域可以扩大的条件，进行量词辖域扩大。任何公式的前束范式都是存在的，但一般说来，并不唯一。利用一阶逻辑等值式以及三条变换规则（置换规则、换名规则、代替规则）就可以求出与公式等值的前束范式，或所谓公式的前束范式。,(1)利用量词转化公式，把否定深入到指导变元的后面。xA(x)xA(x)xA(x)xA(x)(2)利用x(A(x)B)xA(x)B和x(A(x)B)xA(x)B把量词移到全式的最前面，这样便得到前束范式。,例5.6 求公式的前束范式,（1）xF(x)xG(x)xF(x)yG(y)(换名规则)xF(x)yG(y)(5.2)第二式)x(F(x)yG(y)(5.3)第二式)xy(F(x)G(y)(5.3)第二式)（yx(F(x)G(y)）或者xF(x)xG(x)xF(x)xG(x)(5.2)第二式)x(F(x)G(x)(5.5)第一式),例5.6 求公式的前束范式,（2）xF(x)xG(x)xF(x)xG(x)(5.2)第二式)xF(x)yG(y)(换名规则)x(F(x)yG(y)(5.3)第一式)xy(F(x)G(y)(5.3)第一式),说明,公式的前束范式是不唯一的。,例5.7 求前束范式,(1)xF(x)xG(x)yF(y)xG(x)yx(F(y)G(x)(2)xF(x)xG(x)yF(y)xG(x)yx(F(y)G(x)(3)xF(x)xG(x)yF(y)xG(x)yx(F(y)G(x)(4)xF(x)yG(y)xy(F(x)G(x),例5.8 求公式的前束范式,(1)xF(x,y)yG(x,y)tF(t,y)wG(x,w)(换名规则)tw(F(t,y)G(x,w)(5.3),(5.4)或者xF(x,y)yG(x,y)xF(x,t)yG(w,y)(代替规则)xy(F(x,t)G(w,y)(5.3),(5.4),说明,解本题时一定注意，哪些个体变项是约束出现，哪些是自由出现，特别要注意那些既是约束出现又是自由出现的个体变项。不能混淆。,例5.8 求公式的前束范式,(2)(x1F(x1,x2)x2G(x2)x1H(x1,x2,x3)(x4F(x4,x2)x5G(x5)x1H(x1,x2,x3)x4x5(F(x4,x2)G(x5)x1H(x1,x2,x3)x4x5x1(F(x4,x2)G(x5)H(x1,x2,x3),5.3 一阶逻辑的推理理论,在一阶逻辑中，从前提A1,A2,Ak出发推结论B的推理形式结构，依然采用如下的蕴涵式形式A1,A2,Ak B（5.6）若式（5.6）为永真式，则称推理正确，否则称推理不正确。于是，在一阶逻辑中判断推理是否正确也归结为判断（5.6）式是否为永真式了。在一阶逻辑中称永真式的蕴涵式为推理定律，若一个推理的形式结构正是某条推理定律，则这个推理显然是正确的。在一阶逻辑的推理中，某些前提与结论可能是受量词限制，为了使用命题逻辑中的等值式和推理定律，必须在推理过程中有消去和添加量词的规则，以便使谓词演算公式的推理过程可类似于命题演算中推理理论那样进行。,推理定律的来源,命题逻辑推理定律的代换实例由基本等值式生成的推理定律量词分配等值式推理规则量词消去和引入规则,命题逻辑推理定律的代换实例,xF(x)yG(y)xF(x)（化简律的代换实例）xF(x)xF(x)yG(y)（附加律的代换实例）,由基本等值式生成的推理定律,xF(x)xF(x)xF(x)xF(x)xF(x)xF(x)xF(x)xF(x),其他推理定律,xA(x)xB(x)x(A(x)B(x)x(A(x)B(x)xA(x)xB(x)x(A(x)B(x)xA(x)xB(x)x(A(x)B(x)xA(x)xB(x),对x(A(x)B(x)xA(x)xB(x)的讨论若x(A(x)B(x)为真，则有一个客体c，使得A(c)B(c)为真，即A(c)和B(c)都为真，所以xA(x)xB(x)也为真。,推理规律,（1）I16：(x)G(x)(x)G(x)；（2）I17：(x)G(x)(x)H(x)(x)(G(x)H(x)；I18：(x)(G(x)H(x)(x)G(x)(x)H(x)；（3）I19：(x)(G(x)H(x)(x)G(x)(x)H(x)；I20：(x)(G(x)H(x)(x)G(x)(x)H(x)。,推理规律（续）,（4）I21：(x)(y)G(x,y)(y)(x)G(x,y)；I22：(x)(y)G(x,y)(y)(x)G(x,y)；I23：(y)(x)G(x,y)(x)(y)G(x,y)；I24：(y)(x)G(x,y)(x)(y)G(x,y)；I25：(x)(y)G(x,y)(y)(x)G(x,y)；I26：(y)(x)G(x,y)(x)(y)G(x,y)；,量词关系图,等价公式,(x)(y),(y)(x),I22,I23,(y)(x),(x)(y),I24,I21,(x)(y),(y)(x),I25,I26,(y)(x),(x)(y),等价公式,推理规则,为了构造推理系统，还要给出4条重要的推理规则,即消去量词和引入量词的规则：1全称量词消去规则(简记为UI规则或-)2全称量词引入规则(简记为UG规则或+)3存在量词引入规则(简称EG规则或+)4存在量词消去规则(简记为EI规则或-),全称量词消去规则(简记为UI规则或-),含义：如果个体域的所有元素都具有性质A，则个体域中的任一元素具有性质A。两式成立的条件：(1)在第一式中，取代x的y应为任意的不在A(x)中约束出现的个体变项。(2)在第二式中，c为任意个体常项。(3)用y或c去取代A(x)中自由出现的x时，一定要在x自由出现的一切地方进行取代。,全称量词消去规则(简记为UI规则或-),举例,当A(x)为原子公式时，比如A(x)=F(x)，则当xA(x)为真时，对于个体域中任意的个体变项y，不会出现F(y)为假的情况。当A(x)不是原子公式时，如y已在A(x)中约束出现了，就不能用y取代x，否则会出现xA(x)为真而A(y)为假的情况。考虑个体域为实数集合，公式A(x)=yF(x,y)为xy。当对公式xA(x)=xyF(x,y)使用UI规则时，用y取代x，就会得到A(y)=yF(y,y)，即y(yy)，这显然是假命题。原因是违背了条件(1)。若用z取代x，得A(z)=yF(z,y)=y(zy)就不会产生这种错误。,全称量词引入规则(简记为UG规则或+),该式成立的条件是：(1)无论A(y)中自由出现的个体变项y取何值，A(y)应该均为真。(2)取代自由出现的y的x也不能在A(y)中约束出现。,举例,取个体域为实数集，F(x,y)为xy，A(y)=xF(x,y)。显然A(y)满足条件(1)。对A(y)应用UG规则时，若取已约束出现的x取代y，会得到xA(x)=xx(xx)，这是假命题。产生这种错误的原因是违背了条件(2)。若取z取代y，得zA(z)=zx(xz)为真命题。,存在量词引入规则(简称EG规则或+),该式成立的条件是：(1)c是特定的个体常项。(2)取代c的x不能在A(c)中出现过。,举例,取个体域为实数集，F(x,y)为xy，取A(5)=xF(x,5)。显然A(5)是真命题。在应用EG规则时，若用A(5)中已出现的x取代5，得xxF(x,x)=x(xx)，这是假命题。产生这种错误的原因是违背了条件(2)。若用A(5)中未出现过的个体变项y取代5，得yA(y)=yxF(xy)，这为真命题。,存在量词消去规则(简记为EI规则或-),该式成立的条件是：(1)c是使A为真的特定的个体常项。(2)c不在A(x)中出现。(3)若A(x)中除自由出现的x外，还有其它自由出现的个体变项，此规则不能使用。,举例,取个体域为自然数集合，F(x)为x是奇数，G(x)为x是偶数。xF(x)与xG(x)都是真命题，则对于某些c和d，可以断定P(c)Q(d)必定为真，但不能断定P(c)Q(c)是真。对xF(x)使用EI规则时，取代x的c一定是特定的个体常项1,3,5等奇数。对xG(x)使用EI规则时，取代x的c一定是特定的个体常项2,4,6等偶数。,定义5.3 自然推理系统定义,1.字母表。同一阶语言的字母表。2.合式公式。同合式公式的定义。3.推理规则：(1)前提引入规则。(2)结论引入规则。(3)置换规则。(4)假言推理规则。(5)附加规则。(6)化简规则。(7)拒取式规则。(8)假言三段论规则。,(9)析取三段论规则。(10)构造性二难推理规则。(11)合取引入规则。(12)UI规则。(13)UG规则。(14)EG规则。(15)EI规则。,谓词演算的综合推理方法,推导过程中可以引用命题演算中的前提 P和结论T。如果结论是以蕴涵形式(或析取形式)给出，我们还可以附加前提。若需消去量词，可以引用规则UI和规则EI。当所要求的结论可能被定量时，此时可引用规则UG和规则EG将其量词加入。,谓词演算的综合推理方法（续1）,证明时可采用如命题演算中的直接证明方法和间接证明方法。在推导过程中，对消去量词的公式或公式中不含量词的子公式，完全可以引用命题演算中的基本等价公式和基本蕴涵公式。在推导过程中，对含有量词的公式可以引用谓词中的基本等价公式和基本蕴涵公式。,例题,例题 在自然推理系统中，构造下面推理的证明所有的人都是要死的，苏格拉底是人，所以苏格拉底是要死的。解：先将原子命题符号化。设 F(x):x是一个人，G(x):x是要死的，s：苏格拉底。前提：x(F(x)G(x),F(s)结论：G(s)证明：x(F(x)G(x)前提引入 F(s)G(s)UI规则 F(s)前提引入 G(s)假言推理,例,例 设个体域为实数集合，F(x,y)为xy。指出在推理系统F中，以xyF(x，y)(真命题)为前提，推出xF(x,c)(假命题)的下述推理证明中的错误。xyF(x,y)前提引入 yF(z,y)UI规则 F(z,c)EI规则 xF(x,c)UG规则 解 由于c为特定的个体常项，所以xF(x,c)(即为x(xc)为假命题。如果按F中推理规则进行推理，不会从真命题推出假命题。在以上推理证明中，第三步错了，由于F(z,y)中除有自由出现的y，还有自由出现的z，按EI规则应该满足的条件(3)，此处不能用EI规则。用了EI规则，导致了从真命题推出假命题的错误。,(3)错了！,例5.9,例5.9 在自然推理系统中，构造下面推理的证明任何自然数都是整数；存在着自然数。所以存在着整数。个体域为实数集合R。解：先将原子命题符号化。设 F(x):x为自然数，G(x):x为整数。前提：x(F(x)G(x),xF(x)结论：xG(x)证明：xF(x)前提引入 F(c)EI规则 x(F(x)G(x)前提引入 F(c)G(c)UI规则 G(c)假言推理 xG(x)EG规则,正确！,方法2：,证明：x(F(x)G(x)前提引入 F(x)G(x)-F(x)xG(x)+xF(x)xG(x)-xF(x)前提引入 xG(x)假言推理,例5.9说明,以上证明的每一步都是严格按推理规则及应满足的条件进行的。因此，前提的合取为真时，结论必为真。但如果改变命题序列的顺序会产生由真前提推出假结论的错误。如果证明如下进行：x(F(x)G(x)前提引入 F(c)G(c)UI规则 xF(x)前提引入 F(c)EI规则在中取c=,则F()G()为真（前件假）,于是中F()为假，这样从前件真推出了假的中间结果。,例5.10,例5.10 在自然推理系统F中,构造下面推理的证明。前提：x(F(x)G(x),x(F(x)H(x)结论：x(G(x）H(x)提示 在证明序列中先引进带存在量词的前提。,例5.10证明,x(F(x)H(x)前提引入 F(c)H(c)EI规则 x(F(x)G(x)前提引入 F(c)G(c)UI规则 F(c)化简 G(c)假言推理 H(c)化简 G(c)H(c)合取(G(x）H(x)）EG规则,谓词逻辑推理的难点,在推导过程中，如既要使用规则UI又要使用规则EI消去公式中的量词，而且选用的个体是同一个符号，则必须先先使用规则EI，再使用规则UI。然后再使用命题演算中的推理规则，最后使用规则UG或规则EG引入量词，得到所要的结论。如一个变量是用规则ES消去量词，对该变量在添加量词时，则只能使用规则EG，而不能使用规则UG；如使用规则US消去量词，对该变量在添加量词时，则可使用规则EG和规则UG。,谓词逻辑推理的难点（续）,如有两个含有存在量词的公式，当用规则EI消去量词时，不能选用同样的一个常量符号来取代两个公式中的变元，而应用不同的常量符号来取代它们。在用规则UI和规则EI消去量词、用规则UG和规则EG添加量词时，此量词必须位于整个公式的最前端，并且它的辖域为其后的整个公式。,谓词逻辑推理的难点（续）,在添加量词(x)、(x)时，所选用的x不能在公式G(y)或G(c)中自由出现且G(y)或G(c)对x是自由的。在使用规则EG引入存在量词(x)时，此x不得仅为G(c)或G(y)中的函数变元。在使用规则UG引入全称量词(x)时，此x不得为G(y)中的函数变元(因该函数变元不得作为自由变元)。在使用规则UG引入全称量词(x)时，G(y)中不得出现在使用规则UI引入y之后由规则EI引入的常量或函数。,例5.11,例5.11 在自然推理系统F中，构造下面推理的证明：不存在能表示成分数的无理数，有理数都能表示成分数。因此，有理数都不是无理数。个体域为实数集合。,设 F(x):x为无理数，G(x):x为有理数，H(x):x能表示成分数。前提：x(F(x)H(x)，x(G(x)H(x)结论：x(G(x)F(x),解答,例5.11证明,x(F(x)H(x)前提引入 x(F(x)H(x)置换 x(H(x)F(x)置换 H(y)F(y)UI规则 x(G(x)H(x)前提引入 G(y)H(y)UI规则 G(y)F(y)假言三段论 x(G(x)F(x)UG规则,注意x(F(x)H(x)不是前束范式，因而不能对它使用EI规则。因为结论中的量词是全称量词，因而在使用UI规则时用第一式，而不能用第二式。,说明,例,现有一智力测验题目(水容器问题)：设有两个分别能盛7升与5升的水容器，开始时两个容器均空，允许对容器做三种操作：（1）容器倒满水，（2）将容器中的水倒光，（3）从一个容器倒水至另一容器，使一个容器倒光而另一容器倒满。最后要求能使大容器(能盛7升的容器)中有4升水，并求其操作过程。,大容器注满,小容器倒空,解决方案,S(0,0),S(7,0),S(2,5),S(2,0),S(0,2),S(7,2),S(4,5),S(4,0),大容器注满,小容器倒空,小容器注满,小容器注满,倒入小容器,证明,（1）S(0,0)P（2）(x)(y)(S(x,y)S(7,y)P（3）(y)(S(0,y)S(7,y)(2)UI（4）S(0,0)S(7,0)(3)UI（5）S(7,0)(1)(4)T,I（6）(x)(y)(z)(S(x,y)S(z,5)P（7）(y)(z)(S(7,y)S(z,5)(6)UI（8）(z)(S(7,0)S(z,5)(7)UI（9）S(7,0)S(2,5)(8)EI,证明,（10）S(2,5)(5)(9)T,I（11）(x)(y)(S(x,y)S(x,0)P（12）(y)(S(2,y)S(2,0)(11)UI（13）S(2,5)S(2,0)(12)UI（14）S(2,0)(10)(13)T,I（15）(x)(y)(z)(S(x,y)S(0,z)P（16）(y)(z)(S(2,y)S(0,z)(15)UI（17）(z)(S(2,0)S(0,z)(16)UI,证明（续）,（18）(S(2,0)S(0,2)(17)EI（19）S(0,2)(14)(18)T,I（20）(x)(y)(S(x,y)S(7,y)P（21）(y)(S(0,y)S(7,y)(20)UI（22）(S(0,2)S(7,2)(21)UI（23）S(7,2)(19)(22)T,I（24）(x)(y)(z)(S(x,y)S(z,5)P（25）(y)(z)(S(7,y)S(z,5)(24)UI（26）(z)(S(7,2)S(z,5)(25)UI,证明（续）,（27）S(7,2)S(4,5)(26)EI（28）S(4,5)(23)(27)T,I（29）(x)(y)(S(x,y)S(x,0)P（30）(y)(S(4,y)S(4,0)(29)UI（31）S(4,5)S(4,0)(30)UI（32）S(4,0)(30)(33)T,I,本章主要内容,等值式与基本的等值式在有限个体域中消去量词等值式量词否定等值式量词辖域收缩与扩张等值式量词分配等值式基本规则：置换规则、换名规则、代替规则前束范式推理理论：推理的形式结构、推理正确、构造证明新的推理规则：UI、UG、EI、EG,学习要求,深刻理解重要的等值式，并能熟练地使用它们。熟练地使用置换规则、换名规则和代替规则。准确地求出给定公式的前束范式（形式可以不唯一）。正确地使用UI、UG、EI、EG规则，特别地要注意它们之间的关系。一定对前束范式才能使用UI、UG、EI、EG规则，对不是前束范式的公式要使用它们，一定先求出公式的前束范式。记住UI、UG、EI、EG规则的各自使用条件。在同一推理的证明中，如果既要使用UI规则，又要使用EI规则，一定要先使用EI规则，后使用UI规则，而且UI规则使用的个体常项一定是EI规则中使用过的。对于给定的推理，正确地构造出它的证明。,在自然推理系统F中构造推理的证明,前提：xF(x)xG(x)结论：x(F(x)G(x)证明 xF(x)xG(x)前提引入 yF(y)xG(x)置换（换名规则）yx(F(y)G(x)置换 x(F(z)G(x)UI规则 F(z)G(z)UI规则 x(F(x)G(x)UG规则,在自然推理系统F中构造推理的证明,前提：x(F(x)G(x)结论：xF(x)xG(x)证明 xF(x)附加前提引入 F(y)UI规则 x(F(x)G(x)前提引入 F(y)G(y)UI规则 G(y)假言推理 xG(x)UG规则,例题选讲,例题 在自然推理系统F中，构造下面推理的证明：实数不是有理数就是无理数，无理数都不是分数，所以，若有分数，则必有有理数（个体域为实数集合）,设 F(x):x是有理数，G(x):x是无理数，H(x):x是分数。前提：x(F(x)G(x)，x(G(x)H(x)结论：xH(x)xF(x),解答,例题的证明,xH(x)附加前提引入 x(F(x)G(x)前提引入 H(c)EI规则 F(c)G(c)UI规则 x(G(x)H(x)前提引入 G(c)H(c)UI规则 G(c)拒取式 F(c)析取三段论(x)F(x)EG规则,作业,习题五2、3、13、14、15、23,