《谓词演算的推理理论-永真推理系统.ppt》由会员分享，可在线阅读，更多相关《谓词演算的推理理论-永真推理系统.ppt（28页珍藏版）》请在三一办公上搜索。
1、第四章 谓词演算的推理理论,4.1 谓词演算的永真推理系统 4.1.1 公理系统的组成部分 4.1.2 公里系统的推理过程4.2谓词演算的假设推理系统4.3谓词演算的归结推理系统,4.1.1 公理系统的组成部分,一、语法部分(一)基本符号(二)公理(三)规则二、语义部分三、关于公理的几点说明,（一）基本符号,公理系统所允许出现的全体符号的集合。,(1)命题变元：P，Q，R，等字母表示命题变元(2)个体变元：x，y，等小写字母表示个体变元(3)谓词变元：X，Y，等大写字母表示谓词变元(4)联结词：、是联结词(5)量词：全称量词、存在量词(6)括号：(，)是括号(7)全称封闭符：,基本符号（续）,
2、(8)合式公式：(i)原子命题P是合式公式；(ii)谓词填式A(x1，x2，x3，xn)是合式公式；(iii)若A是公式，则A是合式公式；(iv)若A和B是合式公式，则(AB)，(AB)，(AB)，(AB)为公式；(v)若A是合式公式，x是A中出现的任何个体变元，则xA(x)，xA(x)为合式公式；(vi)只有有限次使用(i)、(ii)、(iii)、(iv)、(v)所得到的式子才是合式公式。,基本符号（续）,(9)全称封闭式：设为含有n个自由变元的公式，如果在前用全称量词把n个自由变元约束起来后所得到的公式，称为的全称封闭式。记为。例 写出下式的全称封闭式=xP(x，y)uQ(u，v)解：=(
3、xP(x，y)uQ(u，v)=yv(xP(x，y)uQ(u，v),（二）公理,公理1(PP)公理2(P(QR)(Q(PR)公理3(PQ)(QR)(PR)公理4(P(PQ)(PQ)公理5(PQ)(PQ)公理6(PQ)(QP)公理7(PQ)(QP)(PQ),调头,传递,凝缩,（二）公理,公理8(PQ)P)公理9(PQ)Q)公理10(P(Q(PQ)公理11(P(PQ)公理12(Q(PQ)公理13(PR)(QR)(PQ)R)公理14(PQ)(QP)公理15(PP),（二）公理,公理20(xP(x)P(x)公理21(P(x)x P(x),如果只有一个自由变元，公理20与公理21可以分别理解如下：x(yP
4、(y)P(x)x(P(x)y P(y),（三）规则,(1)分离规则：如果(AB)且A，则B。(2)全称规则：(P(x)(x P(x)(其中中不含自由的x)(3)全称量词消去规则：xP(x)P(x)(x可以为任意的变元)(4)存在量词引入规则：(P(x)(x P(x)(其中中不含自由的x),回顾:量词作用域的收缩与扩张,设公式中不含有自由的x，则下面的公式成立:x(x)=(x(x)x(x)=(x(x)x(x)=(x(x)x(x)=(x(x),存在量词引入,全称量词引入,二、语义部分,(1)公理是永真公式。(2)规则规定如何从永真公式推出永真公式。分离规则指明，如果(AB)永真且A永真，则B也为永
5、真公式。(3)定理为永真公式，它们是从公理出发利用上述规则推出来的公式。,三、关于公理的几点说明,(1)本系统中不引入代入规则，它的作用由下面的(2)来实现；(2)本系统中的所有公理我们把它看作公理模式，即只要形如某一公理，我们就称其为某一公理。如(PP)、(P(QR)(P(QR)、(xP(x)x P(x)等均为公理1。,第四章 谓词演算的推理理论,4.1 谓词演算的永真推理系统 4.1.1 公理系统的组成部分 4.1.2 公里系统的推理过程4.2谓词演算的假设推理系统4.3谓词演算的归结推理系统,例1(p41)已知定理(P(QP),求证:全0规则(x)x(x),证明：(1)(x)(2)(x)
6、(PP)(x)引用定理(3)(PP)(x)(2)(1)分离(4)(PP)x(x)全称规则(3)(5)(PP)公理(1)(6)x(x)(4)(5)分离则有全0规则(x)x(x),全n规则、存n规则,全n规则：(1(2(n(x)(1(2(nx(x)存n规则：(1(2(n(x)(1(2(n(x(x),全1规则=全称规则,存0规则=存在规则,例 试利用存0规则求证存1规则,(1(x)(1(x(x),证明：(1)(1(x)(2)(1(x)(x)(1)公理2(3)(x)(1)分离(1)(2)(4)(x(x)(1)存0规则(5)(x(x)(1)(1(x(x)公理2(6)(1(x(x)分离(5)(6),两次运
7、用调头公理2,例(练习4.1(1)x(P(x)(xP(x),证明:x(P(x)(P(x)公理20:P(x)与P(x)同形(2)x(P(x)(x P(x)全2规则,(1(2(x)(1(2x(x),例(续)x(P(x)(x P(x),再证明(x P(x)x(P(x)证明:(3)xP(x)P(x)公理20(4)(xP(x)P(x)(xP(x)(P(x)定理(5)(xP(x)(P(x)分离(3)(4)(6)(xP(x)x(P(x)全1规则,定理(PQ)(RP)(RQ),例(再续)x(P(x)(x P(x),已经证得(2)(6)两式(2)x(P(x)(x P(x)(6)(xP(x)x(P(x)于是(7)
8、(x(P(x)(x P(x)(xP(x)x(P(x)(x(P(x)(x P(x)公理7(8)(xP(x)x(P(x)(x(P(x)(x P(x)分离(2)(7)(9)x(P(x)(x P(x)分离(6)(8),例(练习4.1(2)x(P(x)(x P(x),先证明 x(P(x)(x P(x)证明:(1)x(P(x)(P(x)公理20(2)x(P(x)(x P(x)存1规则,1(P(x)1(xP(x),例(续)x(P(x)(x P(x),再证明(x P(x)x(P(x)证明:(3)P(x)xP(x)公理21(4)(P(x)xP(x)(xP(x)(P(x)公理3(5)(xP(x)(P(x)分(3)
9、(4)(6)(xP(x)x(P(x)全称规则,例(再续)x(P(x)(x P(x),已经证得(2)(6)两式(2)x(P(x)(x P(x)(6)(xP(x)x(P(x)于是有(7)(x(P(x)(x P(x)(xP(x)x(P(x)(x(P(x)(x P(x)公理7(8)(xP(x)x(P(x)(x(P(x)(x P(x)分离(2)(7)(9)x(P(x)(x P(x)分离(6)(8),例(练习4.2)已知公理(A)(P(QP)(B)(PP)及分离规则和全称规则，全称规则为：(1(2(x)(1(2x(x)试证：全0规则(x)x(x),证:(1)(x)(2)(P(QP)公理A(3)(x)(PP
10、)(x)代入(1)(4)(PP)(x)(1)(3)分离(5)(PP)(x)(PP)(PP)(x)代入(2)(6)(PP)(PP)(x)(4)(5)分离(7)(PP)(PP)x(x)全称规则(8)(PP)公理B(9)(PP)x(x)(7)(8)分离(10)(x(x)(9)(8)分离,例2(p42)试证明：(A)(xP(x)xP(x),证(A)(1)(xP(x)P(x)公理20(xP(x)P(x)(P(x)xP(x)公理14(3)(P(x)xP(x)(2)(1)分离(4)(xP(x)xP(x)存在量词引入规则(3)(xP(x)xP(x)(xP(x)xP(x)公理14(6)(xP(x)xP(x)(5
11、)(4)分离,例2(p42)已知定理：(PQ)(QP),试证明：(B)(xP(x)xP(x),证(B)(7)(P(x)xP(x)公理21(8)(P(x)xP(x)(xP(x)P(x)已知定理(9)(xP(x)P(x)(8)(7)分离(10)(xP(x)x P(x)全称规则(9),例2(p42)试证明：(xP(x)xP(x),证明：已经分别证出如下(6)(10)两式(xP(x)xP(x)(10)(xP(x)x P(x)(11)(xP(x)xP(x)(xP(x)x P(x)(xP(x)xP(x)公理7(12)(xP(x)xP(x)(xP(x)xP(x)(11)(6)分离(13)(xP(x)xP(x)(12)(10)分离,例4(p43)(PQ(x)(PxQ(x),证明：(1)(Q(x)xQ(x)公理21(2)(PQ(x)(Q(x)xQ(x)(PxQ(x)公理3(3)(PQ(x)(Q(x)xQ(x)(PxQ(x)(Q(x)xQ(x)(PQ(x)(PxQ(x)公理2(4)(Q(x)xQ(x)(PQ(x)(PxQ(x)(2)(3)分离(5)(PQ(x)(PxQ(x)(1)(4)分离,第四章 谓词演算的推理理论,4.1 谓词演算的永真推理系统 4.1.1 公理系统的组成部分 4.1.2 公里系统的推理过程4.2谓词演算的假设推理系统4.3谓词演算的归结推理系统,
