《谓词逻辑的等值和推理演算教学教材》由会员分享，可在线阅读，更多相关《谓词逻辑的等值和推理演算教学教材（45页珍藏版）》请在金锄头文库上搜索。
1、谓词逻辑的等值和推理演算,Lu Chaojun, SJTU,2,主要内容,谓词公式的等值 等值演算 范式(PNF, Skolem范式) 推理式及推理演算 归结推理,Lu Chaojun, SJTU,3,公式的等值,谓词公式和如果在任一解释下都有相同的真值,就说和是等值的(或等价),记作 (或 ). 定理 iff 是普遍有效的,Lu Chaojun, SJTU,4,由命题逻辑移植来的等值式,在命题逻辑的等值式中以谓词公式代入命题变项,便可得谓词逻辑的等值式. 例如: p p (x)P(x) (x)P(x) pq p q P(x)Q(x) P(x) Q(x),4,Lu Chaojun, SJTU,
2、6,量词分配等值式,量词对及的分配律 (x)(x) (x)(x) (x)(x) (x)(x) (x)(x) (x)(x) (x)(x) (x)(x) 其中 不含自由x ! 这个条件很容易满足:对约束变元改名即可.,6,Lu Chaojun, SJTU,7,量词分配等值式(续),量词对的分配律 (x)(x) (x)(x) (x)(x) (x)(x) (x)(x) (x)(x) (x)(x) (x)(x) 其中 不含自由x !,7,Lu Chaojun, SJTU,8,量词分配等值式(续),对, 对的分配律 (x)(x)(x) (x)(x)(x)(x) (x)(x)(x) (x)(x)(x)(x)
3、 对, 对没有分配律 举例说明: (x)(Man(x)Woman(x) 所有人要么是男人要么是女人. (x)Man(x)(x)Woman(x) 要么所有人都是男人,要么所有人都是女人.,8,Lu Chaojun, SJTU,9,量词分配等值式(续),回顾:约束变元易名规则 (x)(x) = (y)(y) (x)(x) = (y)(y) 变元易名后的“分配律” (x)(y)(x)(y) = (x)(x)(x)(x) (x)(y)(x)(y) = (x)(x)(x)(x),9,Lu Chaojun, SJTU,10,范式,回顾:命题逻辑公式有与之等值的范式. 谓词逻辑公式也有范式,其中前束范式与原
4、公式是等值的,而其他范式与原公式只有较弱的关系.,Lu Chaojun, SJTU,11,前束范式,定义:如果公式 中的所有量词都非否定地置于公式左端,且其辖域都延伸到公式的末端,则称是前束范式(prenex normal form).形如 (Q1x1)(Qnxn) M(x1, xn) 其中诸Qi为量词或, M不含量词,称为 的母式(基式, matrix). 前束范式定理:任一公式都有与之等值的PNF.,Lu Chaojun, SJTU,12,如何转化成PNF,1.消去和 2.否定词内移 应用De Morgan律 3.约束变元易名(如果必要的话) 4.量词左移 应用分配等值式,Lu Chaoj
5、un, SJTU,13,例:求PNF,(x)(y)P(a,x,y)(x)(y)Q(y,b)R(x) = (x)(y)P(a,x,y)(x)(y)Q(y,b)R(x) = (x)(y)P(a,x,y) (x)(y)Q(y,b) R(x) = (x)(y)P(a,x,y) (x)(y)Q(y,b) R(x) = (x)(y)P(a,x,y) (y)Q(y,b) R(x) = (x)(y)P(a,x,y) (z)Q(z,b) R(x) = (x)(y)(z)(P(a,x,y) Q(z,b) R(x) = (x)(z)(y)(P(a,x,y) Q(z,b) R(x) = (x)(y)(z)(P(a,x
6、,y)Q(z,b)R(x)(pp),13,Lu Chaojun, SJTU,14,Skolem范式,前束范式对前束量词没有次序要求,也没有其他要求. 如果对前束范式进而要求所有都在之左,或者只保留而消去,便得Skolem范式的两种形式.,Lu Chaojun, SJTU,15,Skolem范式(1):-前束范式,一个公式的-前束范式形如 (x1)(xi)(xi+1)(xn)M(x1,xn) 是前束范式 至少有一个存在量词 存在量词都在全称量词的左边 M(x1,xn)中不再有量词,也无自由个体变项,Lu Chaojun, SJTU,16,-前束范式定理,定理:任一公式都可化为-前束范式 ,并且
7、普遍有效 iff 普遍有效. 说明: 只有普遍有效的公式 ,才与其-前束范式是等值的. 一般的公式与其-前束范式并不等值. 用于FOL完备性的证明.,Lu Chaojun, SJTU,17,例:-前束范式,求(x)(y)(u)P(x,y,u)的-前束范式(P中无量词). 1.先求前束范式.本例已是. 2.关键一步:(y)改写成(y).(z).形如 (x)(y)(u)(P(x,y,u) S(x,y) (z)S(x, z) 引入新谓词S和新变元z.(直观意义?) 3.(z)左移即得结果: (x)(y)(u)(z)(P(x,y,u) S(x,y) S(x, z) 当有多个在的左边,可按此法逐一右移.
8、,Lu Chaojun, SJTU,18,Skolem范式(2),PNF中消去所有而只保留. 术语“Skolem范式”一般指这种形式. 定理:任一公式 都可化为Skolem范式 ,并且 (不)可满足 iff (不)可满足. 不是等值(equivalent),而是“等可满足” (equisatisfiable).,Lu Chaojun, SJTU,19,例:Skolem范式,(x)(y)(z)(u)(v)(w)P(x,y,z,u,v,w) 1.先求前束范式.本例已是. 2.关键:消去.方法是引入个体常项或函数.如 (y)(z)(u)(v)(w)P(a,y,z,u,v,w) 消去x:引入新个体常项
9、a代入x 3.消去(u)时,引进的个体因为与左边的y和z有关,所以不能用个体常项,而是用函数 (y)(z)(v)(w)P(a,y,z,f(y,z),v,w) 4.消去(w): (y)(z)(v)P(a,y,z,f(y,z),v, g(y,z,v),Lu Chaojun, SJTU,20,例:Skolem范式不保持等值,比较(x)(y)P(x,y)与(x)P(x, f(x): 在1,2域上 (x)(y)P(x,y) = (P(1,1) P(1,2) (P(2,1) P(2,2) (x)P(x, f(x) = P(1, f(1) P(2, f(2) 两者明显不等值.但在(不)可满足的意义下两者是一
10、致的.,Lu Chaojun, SJTU,21,谓词逻辑的推理,命题逻辑中有关推理形式、重言蕴涵以及基本的推理公式的讨论和所用的术语都可引入到谓词逻辑中,并可把命题逻辑的推理作为谓词逻辑的推理的一个部分来看待. 这里我们讨论谓词逻辑所特有的推理形式和基本推理公式.,Lu Chaojun, SJTU,22,推理形式,推理形式是指(用)表达推理的公式. 推理形式表达的推理有正确的也有错误的. 例1:所有整数都是有理数,所有有理数都是实数,所以所有整数都是实数. 将这三句话形式化表示,可得如下推理形式: (x)(Integer(x)Rational(x) (x)(Rational(x)Real(x)
11、 (x)(Integer(x)Real(x) 这是正确的推理形式 在命题逻辑里只能表达成p q r,显然不是正确的推理形式.,Lu Chaojun, SJTU,23,推理形式:更多例子,例2:人皆有死,孔子是人,所以孔子有死. (x)(Man(x)Mortal(x) Man(Confucius) Mortal(Confucius) 例3:若有一个又高又胖的人,则有一个高个子而且有一个胖子. (x)(Tall(x)Fat(x) (x)Tall(x) (x)Fat(x) 例4:若某个体a具有性质E,那么所有个体x都具有性质E. E(a)(x)E(x) 这是错误的推理形式,Lu Chaojun, S
12、JTU,24,基本推理式,(1) (x)P(x) (x)Q(x) (x)(P(x) Q(x) (2) (x)(P(x) Q(x) (x)P(x) (x)Q(x) (3) (x)(P(x) Q(x) (x)P(x) (x)Q(x) (4) (x)(P(x) Q(x) (x)P(x) (x)Q(x) (5) (x)(P(x) Q(x) ) (x)P(x) (x)Q(x) (6) (x)(P(x) Q(x) (x)P(x) (x)Q(x) (7) (x)(P(x)Q(x)(x)(Q(x)R(x)(x)(P(x)R(x) (8) (x)(P(x) Q(x) P(a) Q(a) (9) (x)(y)P(
13、x,y) (x)(y)P(x,y) (10) (x)(y)P(x,y) (y)(x)P(x,y),Lu Chaojun, SJTU,25,举例说明基本推理式,(2) (x)(P(x) Q(x) (x)P(x) (x)Q(x) 语义说明:若个体域是某班学生,P(x)表示x是高材生,Q(x)表示x是运动健将,那么(x)(P(x) Q(x)表示有学生既是高材生又是运动健将,而(x)P(x) (x)Q(x)是说有高材生并且有运动健将(但不要求高材生和运动健将是同一个学生). 显然推理式(2)成立. 因为结论比前提弱,推理式(2)的逆不成立.,Lu Chaojun, SJTU,26,推理演算,命题逻辑中
14、的推理演算可推广到谓词逻辑.推理规则(代入规则需补充说明)都可直接移入谓词逻辑. 除此之外,还需引入4条有关量词的推理规则.,Lu Chaojun, SJTU,27,消去规则,消去规则: (x)(x) (y) y是个体变元,代表论域中任一个体. (y)是在(x)中对x代入y的结果. 当(x)中不含量词和其他变项时成立. 当允许(x)中出现量词和变项时,则需限制y不在(x)中约束出现. 例如: (x)(z)(xz)在实数上成立,于是(z)(yz)也成立. 但若将y取为z,便有(z)(zz),这是矛盾式.,Lu Chaojun, SJTU,28,引入规则,引入规则: (y) (x)(x). y是论
15、域中任一个体 显然若任一个体y(自由变项)都使 为真,那么(x)(x)为真. x不在(y)中出现. 例如: (z)(zy)在实数域上成立,则(x)(z)(zx)也成立. 但若引入(z),(z)(z)(zz)是不成立的.,Lu Chaojun, SJTU,29,消去规则,消去规则: (x)(x) (c) 其中c是未出现的个体常项 如果存在个体使(x)为真,那么就让c是那个个体,自然(c)为真. 这是数学里常用的存在推理法. 需限制(x)(x)中没有自由个体变元出现. 例如:实数域上(x)(xy)成立.由于y是自由个体变元,这时不能推导出cy. 还需限制(x)中不含有c. 例如在实数域上(x)(c
16、x)是成立的,但cc不成立.,Lu Chaojun, SJTU,30,引入规则,引入规则: (c) (x)(x) 其中c是个体常项. 意指如果有个体常项c使为真,那么(x)(x)也为真. 需限制x不出现在(c)中. 例如实数域上(x)(x0)成立,但(x)(x)(xx)不成立.,Lu Chaojun, SJTU,31,使用中的注意事项,多个量词下的量词消去与引入规则: (x)(y)(x,y) (y)(x,y) 右端不能写成(y)(y,y) (x)(x,c) (y)(x)(x,y) 右端不能写成(x)(x)(x,x) (x)(y)(x,y) (y)(x,y) (x,c) 但不能再反推出(x)(x,c)和(y)(x)(x,y) 原因是(x)(y)(x,y)成立时,对每个x所找到的y是依赖于x的,从而(x,y)的成立是有条件的,不是对所有的x都有同一个y.,Lu Chaojun, SJTU,32
