《谓词演算的推理理论-永真推理系统》由会员分享,可在线阅读,更多相关《谓词演算的推理理论-永真推理系统(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个自由变元 约束起来后所得到的公式,称为的全称 封闭式。记为。 例 写出下式的全称封闭
3、式 =xP(x,y)uQ(u,v)解: =(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
4、 (P(x)x P(x)如果只有一个自由变元,公理20与公理21可以分 别理解如下:x(yP(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(
5、x)存在量 词引入全称量 词引入二、语义部分 (1) 公理是永真公式。(2) 规则规定如何从永真公式推出永真公式。分离规则指明,如果(AB)永真且A 永真,则B也为永真公式。(3) 定理为永真公式,它们是从公理出发利用 上述规则推出来的公式。三、关于公理的几点说明(1) 本系统中不引入代入规则,它的作用由下 面的(2)来实现;(2) 本系统中的所有公理我们把它看作公理模 式,即只要形如某一公理,我们就称其为 某一公理。如 (PP)、(P(QR)(P(QR)、(xP(x)x P(x)等均为公理1。第四章 谓词演算的推理理论4.1 谓词演算的永真推理系统4.1.1 公理系统的组成部分4.1.2 公
6、里系统的推理过程4.2谓词演算的假设推理系统 4.3谓词演算的归结推理系统例1 (p41)已知定理(P(QP),求证: 全0规则(x)x(x)证明: (1) (x) (2) (x)(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
7、)证明: (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)两次运用调头公理2例(练习4.1(1) x(P(x)(xP(x) 证明: (1)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)
8、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) (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)
9、分离(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)(4)(6) (xP(x)x(P(x) 全称规则例(再续) x(P(x)(x P(x)已经证得(2)(6)两式 (2) x(P(x) (x P(x) (6)
10、(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) (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