离散数学(一阶逻辑等值演算与推理)

1、1,第五章 一阶逻辑等值演算与推理,一阶逻辑等值式与基本的等值式 置换规则、换名规则、代替规则 前束范式 自然推理系统NL及其推理规则,铺该涛廓站阅费瓜扩其换闭堕轮粳室英过柔珐锅瑶厂岩叫闪饱蛹垒根帮晚离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),2,5.1 一阶逻辑等值式与置换规则,定义5.1 设A, B是两个谓词公式, 如果AB是永真式, 则称A与B等值, 记作AB, 并称AB是等值式. 由定义显然可以看出：公式A，B等值的充要条件是：对A，B的任意解释I，A，B在I下的真值相同。 因为对任意公式A，B，在解释I下，A，B就是两个命题，所以命题逻辑中给出的基本等价式，

2、在谓词逻辑中仍然成立。,逝陌还渝酝昧力篓狰格镁妙跌弃枚财罚姐七供弱琳埔衣番癌若搅余甭所亨离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),3,基本等值式,第一组 命题逻辑中16组基本等值式的代换实例 例如，xF(x)xF(x), xF(x)yG(y) xF(x)yG(y) 等 判断下列公式的类型： （1）xP(x) (xyQ(x,y) xP(x) （2）xP(x) (xP(x) yG(y) （3） (P(x,y) Q(x,y) Q(x,y),永真式,永真式,矛盾式,扩肚惕幕谁棺峪黑泊下果霞塔絮审窟社低舅汕蠕牢社满狼晃鄂潦简啼折伸离散数学(一阶逻辑等值演算与推理)离散数学(一

3、阶逻辑等值演算与推理),4,基本等值式,第二组 (1) 消去量词等值式 设D =a1, a2, , an xA(x) A(a1)A(a2)A(an) xA(x) A(a1)A(a2)A(an),设个体域 A=a,b, 公式 (x)P(x) (x)S(x)在A上消去量词后应为:,例,P(a)P(b)(S(a)S(b),妥宅想痕泼脱萍竖膨玫泅逆尖断枉漫操桅欣钝哆噪儿英歌法等割巢些辱虞离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),5,基本等值式,(2) 量词否定等值式 xA(x) xA(x) xA(x) xA(x),例,设论域为人，P(x): x来上课，P(x): x没来上课

4、 xP(x):所有人都来上课 xP(x):不是所有人都来上课 xP(x): 有人没来上课 xP(x):有人来上课 xP(x):没有人来上课 xP(x): 所有人都没来上课,早聋刨党舔铲走敲挟积团逸盔棕抹啄虾忧镍泌三抗竞心人和迈匝与瀑妊僳离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),6, xA(x) xA(x)的证明,对于任意给定的解释I，若I使xA( x)为真，则I使xA(x)为假。则必有某一个x0D，A(x0) 是假命题，于是A(x0) 是真命题，即 xA(x)在I下是真命题，故I使xA(x)为真。 若I使xA(x)为假，则I使xA(x)为真。即对任意的xD，有A(x

5、)是真命题。也就是对任意的xD，A(x)是假命题，于是xA(x)是假命题，故I使xA(x)为假。,疫跺斜音枢炬摆滑促唉幸阵灸你倔砖艰库穿粕桥须疟幕乃茫嫩辛突可石抨离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),7,实例,例1 将下面命题用两种形式符号化, 并证明两者等值: (1) 没有不犯错误的人 解 令F(x)：x是人，G(x)：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) 置换 x(F(x)G(x) 置换,撕粮肛阿弊萌汰奖叶铬葵青栅诸汰紊遥春秃馋镣左蹬少粘粕折垮碎疾刹减离散

6、数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),8,实例,(2) 不是所有的人都爱吃面包 解 令F(x)：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) 置换 x(F(x)G(x) 置换,啸漆报临督瞒诌耪棵有屏枚擅躯烛还丢椽喧乞吸狠锻微规瞎混酵屏边梦山离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),9,量词否定等值式（续）,设个体域中的客体变元为a1,a2,an，则,俺悟粕褪息呜仇舶戎偷常置诬磐增亢晋甥条蚂傲潞辨夸惑馋吻羹蛊戴庸鹏离散数学(一阶

7、逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),10,基本等值式,(3) 量词辖域收缩与扩张等值式. 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),晌涵俯落戴告漆激侯罚姨镍洼途嫌枣胸烧酶牟览巷吠猎厂失惭北挚乐井宰离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),11, x(A(x)B) xA(x)B的证明,设I是A(x)和B的一个解释。若x(A(x)B)在I下取1值，则在I下，对任意xD，A(x)B都是真命

8、题。若B是真命题，则xA(x)B是真命题；若B是假命题，则必然是对每个xD，A(x)都是真命题，故xA(x)取1值。所以xA(x)B在I下取1值。 若x(A(x)B)在I下取0值，则必有一个x0D，使A(x0) B在I下取0值。故A(x0)为假命题，并且B为假命题。所以xA(x)取0值。从而xA(x)B在I下取0值。,拔整茶啤肌妊梳透覆逛荫始扑钳样押赖雁磐每倪艇孕幕钳颈猿坍休蕾镀赌离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),12,基本等值式,关于存在量词的： x(A(x)B) xA(x)B x(A(x)B) xA(x)B x(A(x)B) xA(x)B x(BA(x)

9、 BxA(x),独乘遥体琐赋簇骏站漆妻镜尼吁掺东拿哉捆琳凛芒孜钡郝署淹幸罪瞻淀伸离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),13, x(A(x)B) xA(x)B的证明,设I是A(x)和B的一个解释。若x(A(x)B)在I下取1值，则在I下，存在x0 D，A(x0)B是真命题。若B是真命题，则xA(x)B是真命题；若B是假命题，则必然有A(x0) 是真命题，故xA(x)取1值。所以xA(x)B在I下取1值。 若x(A(x)B)在I下取0值，则在I下对任意的xD，使A(x)B在I下取0值。故A(x)和B都为假命题，所以xA(x)B在I下取0值。,酮隋祟婶印壶读哈舌射箍海

10、颇且垂鳞纵乎芯湃涕诛阁据竖潘辐迫羞毒韩诬离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),14,基本等值式,(4) 量词分配等值式 x(A(x)B(x) xA(x)xB(x) x(A(x)B(x) xA(x)xB(x) 注意：对，对无分配律,栖瘴怖房档八臼朽谤野妄璃答伯档顿翱贺烛瓶未见袁才蚁痪冠载夫慷氦辐离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),15, x(A(x)B(x) xA(x)xB(x),设I是A(x)和B(x)的一个解释。若xA(x)xB(x)在I下取1值，则在解释I下，对任意xD，A(x)、B(x)都是真命题，所以A(x)B(x)是真

11、命题，即对任意xD， A(x)B(x)是真命题，所以x(A(x)B(x)在I下取1值。 若xA(x)xB(x)在I下取0值，则xA(x)为假，或xB(x)为假，若xA(x)为假，必有一个x0D，使A(x0) 在I下取0值，所以A(x0) B(x0)为假命题，所以x(A(x)B(x)在I下取0值。若xB(x)为假，同理可证。,鼻楼兜童驹恳宋谍厢晦择酒类扩昧插懊匝省篙萎这改遭唐磷斡氨宝上休剩离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),16,置换规则、换名规则、代替规则,1. 置换规则：设(A)是含A的公式, 那么, 若AB, 则(A)(B). 2. 换名规则：设A为一公式

12、，将A中某量词辖域中个体变项的所有约束出现及相应的指导变元换成该量词辖域中未曾出现过的个体变项符号，其余部分不变，设所得公式为A，则AA. 3. 代替规则：设A为一公式，将A中某个个体变项的所有自由出现用A中未曾出现过的个体变项符号代替，其余部分不变，设所得 公式为A，则AA.,眠木栖缄螺雨脏伐毋京韵姿炬纶夸熏明冈屹胆齿椽煞好易酮鹤逮耍诸躲犁离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),17,约束变元的换名,约束变元的换名规则： 换名范围:量词中的指导变元和作用域中出现的该变元.公式中其余部分不变. 要换成作用域中没有出现的变元名称.,例：,虚箕螺钒萍肮框熏陋挽租氧械茵

13、删悦孤或蘸远乐劈岂阮凤晶仲唯掌贩侠墓离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),18,自由变元的代替,自由变元代替的规则： 对该自由变元每一处进行代替. 代替的变元与原公式中所有变元名称不能相同.,例：,枯埃屈烦费壳蛤靳趣薯逐枯谴沼赤璃补洒沿沟石铀嘎应哺设算家鼓聊陛葱离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),19,实例,例2 将公式化成等值的不含既有约束出现、又有自由出现的个体变项: x(F(x,y,z)yG(x,y,z) 解 x(F(x,y,z)yG(x,y,z) x(F(x,y,z)tG(x,t,z) 换名规则 xt(F(x,y,z)G

14、(x,t,z) 辖域扩张等值式 或者 x(F(x,y,z)yG(x,y,z) x(F(x,u,z)yG(x,y,z) 代替规则 xy(F(x,u,z)G(x,y,z) 辖域扩张等值式,晨均喝矗鲜俄助练剪妙编柯支侍厄发泵爵佐陷蒂址畔平植碑都虑浴撞洼吟离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),20,实例,例3 设个体域D=a,b,c, 消去下述公式中的量词: (1) xy(F(x)G(y) (2) xyF(x,y),解 xy(F(x)G(y) (y(F(a)G(y)(y(F(b)G(y) (y(F(c)G(y) (F(a)G(a)(F(a)G(b)(F(a)G(c) (

15、F(b)G(a)(F(b)G(b)(F(b)G(c) (F(c)G(a)(F(c)G(b)(F(c)G(c),寒腺怯鼓筹怂摊型拿狞啸彦喳筑仲有庭啄铁倘者部娶碎感四吊创沪僳聘老离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),21,实例,解法二 xy(F(x)G(y) x(F(x)yG(y) 辖域缩小等值式 x(F(x)G(a)G(b)G(c) (F(a)G(a)G(b)G(c) (F(b)G(a)G(b)G(c) (F(c)G(a)G(b)G(c),毡踢镀沃施悲紫歹撼咸砸撅臻崔邯裔赫可护庆瞳踏愈戈侦久满迫恤唐华荚离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与

16、推理),22,实例,(2) xyF(x,y) 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),估邮掂榷叁添侠筑瓶烫臀菇作汕汲幂斜嫌遍晒翻翁硅忍斟腰筐需促掳背郧离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),23,5.2 一阶逻辑前束范式,定义5.2 设A为一个一阶逻辑公式，若A具有如下形式 Q1x1Q2x2QkxkB则称A为前束范式，其中Qi (1 i k)为或，B为不含量词的公式. 例如， x(F(x)G(x) xy(F(x)(G(y)H(

17、x,y) 是前束范式 而 x(F(x)G(x) x(F(x)y(G(y)H(x,y) 不是前束范式，,莽佰徘贞颂嘿丸驳景伦疽蝴兢了纪羹嘎直牺匝膝击谴崩欧恤汤秉膝盒滋麓离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),24,前束范式存在定理,定理5.1（前束范式存在定理）：一阶逻辑中的任何公式都存在与之等值的前束范式 例4 求下列公式的前束范式 (1) x(M(x)F(x) 解 x(M(x)F(x) x(M(x)F(x) （量词否定等值式） x(M(x)F(x) 后两步结果都是前束范式，说明公式的前束范式不惟一.,汉棵萧侣国暇沽刊蔼渊士后件裤腿偶签示羞呸咸砷佩退诗捏桥砒孜搽溺

18、深离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),25,求前束范式的实例,(2) xF(x)xG(x) 解 xF(x)xG(x) xF(x)xG(x) （量词否定等值式） x(F(x)G(x) （量词分配等值式） 或 xF(x)xG(x) xF(x)xG(x) 量词否定等值式 xF(x)yG(y) 换名规则 xy(F(x)G(y) 辖域收缩扩张规则,老坍帅搅乒淮诵阶壶槽赃坛佩冀如钉杨茎柏呜习伎忱合吠抛恕枣弦鳃危挽离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),26,求前束范式的实例,(3) xF(x)y(G(x,y)H(y) 解 xF(x)y(G(x

19、,y)H(y) zF(z)y(G(x,y)H(y) 换名规则 zy(F(z)(G(x,y)H(y) 辖域收缩 扩张规则 或 xF(x)y(G(z,y)H(y) 代替规则 xy(F(x)(G(z,y)H(y),垂筐祷沁短宴脚炒妙串钢筋在何钻宴裂革智锦域婪动榔僚馒再怯哉找蔼死离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),27,求前束范式的实例,醛碱豆骇玫孤丢疏阁操决扬蔗云马与法权炎拱灯玲蕉款员籍报奏合游金冗离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),28,求前束范式的实例,剿锭米攒婶满炉免吉募溺酮出欣随鸦详爵步娇亨冒趣供俺贩骄蹲抬种巫睁离散数学(一

20、阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),29,求前束范式的实例,脖夺胸绳伪鳖贺忙叔较谱瘴乳服借凄拓瓷釉蝗票帽焕棘砌裕菏酵灌玻儡漱离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),30,求前束范式的实例,1. 否定深入。,2. 改名，把量词提到前面。,让赤忙帆瘤张磋富娄寥以兰观反煤镑奈砌狠裳碗橇您就玛屏父单针榴尹砂离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),31,Skolem范式,设G是一个公式，Q1x1QnxnM是与G等价的前束范式，其中M为合取范式形式。若Qr是存在量词，并且它左边没有全称量词，则取异于出现在M中所有常量符号的常

21、量符号c，并用c代替M中所有的xr，然后在首标中删除Qrxr。 若Qs1, , Qsm是所有出现在Qrxr左边的全称量词(m1，1s1s2smr)，则取异于出现在M中所有函数符号的m元函数符号f(xs1,xsm )，用f(xs1,xsm )代替出现在M中的所有xr，然后在首标中删除Qrxr。,英役芳表瘤帅支匣恒外锑毯窖炙搁设度挛崇话午约僻瞅爱券锅碌假会贾寝离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),32,Skolem范式,对首标中的所有存在量词做上述处理后，得到一个在首标中没有存在量词的前束范式，这个前束范式就称为公式G的Skolem范式。其中用来代替xr的那些常量符

22、号和函数符号称为公式G的Skolem函数。,壶杂燃赶磷怔稳毯廓璃段诺址肺觅巡豆佰对轰斋娃孜卖印憾狄秒泪悄翠帮离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),33,实例,G=xyzuvwP(x,y,z,u,v,w) 用a代替x，用f(y, z)代替u，用g(y, z, v)代替w，得公式G的Skolem范式：yzvP(a,y,z,f(y,z),v,g(y,z,v),顽闲咯大彦郸误故霞翘桔曹戏竿煮嵌初苑旺渺耘颗可币颅穷嫡毛睡贪臆渣离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),34,实例,设G=xyP(x，y)，则G的Skolem范式为S=xP(x，f(

23、x),则I1是满足S的解释，且不看对函数的解释， 也是满足G的解释。,吊竹铸甜嘘汽惯孤丰帮婚骋理浦估蘸闷合卤俏犁傲仔遥彰植颧寺惺庐怜韧离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),35,实例,则I2 不看对函数的解释是满足G的解释，也是 满足S的解释，,G与S可满足性等价。,注意,壹灭梨樱匆烙午膨忠神剧汕条刷淌补翟免并瘸馒博十圈迂孵溺倡扫敌斌监离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),36,实例,但是满足G的解释I，不一定满足S，因为在扩充时，可随意指定Skolem函数的值。,G与S不等价，但G与S的可满足性等价,注意,炉莱吼续允渴试椭卉喘汞

24、文履饼荧地善刃推膝喂拽巨联秸溉伪揽浚汪酗膘离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),37,5.3 一阶逻辑的推论理论,推理的形式结构 1. A1A2Ak B 若此式是永真式, 则称推理正确, 记作A1A2Ak B 2. 前提: A1, A2, Ak 结论: B 推理定理: 永真式的蕴涵式,浑泻辗阳学君多半怔世渝阉谆淬术郭赋沃野订汤轻猩朵苞振枫灾致卉惮郭离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),38,推理定理,第一组 命题逻辑推理定理的代换实例 如, xF(x)yG(y) xF(x) 第二组 基本等值式生成的推理定理 如, xF(x) xF

25、(x), xF(x) xF(x) xF(x)xF(x), xF(x) xF(x) 第三组 其他常用推理定律 (1) xA(x)xB(x) x(A(x)B(x) (2) x(A(x)B(x)xA(x)xB(x) (3) x(A(x)B(x) xA(x)xB(x) (4) x(A(x)B(x) xA(x)xB(x),腥嘻运贞现日动稍蹬蹄制窝怀刃右重摧遗蚀姓鞍槽陈漓嚏逆裂灼使算咽怨离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),39,全称量词消去规则,1. 全称量词消去规则(-) 或 其中x,y是个体变项符号, c是个体常项符号, 且在A中x不在y和y的辖域内自由出现。,龋卵桓

26、峪钱屉江柳响檄暗蹲适颓莫陶喉唉吁奶易痘斜骋宴预书古殷佯耐牢离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),40,重要提示,反例1：设个体域为R, F(x,y):xy， xyF(x,y)为真命题。 “证明” xyF(x,y)前提引入 yF(y,y) - 结论为假命题。 原因：在yF(x,y)中x自由出现在y的辖域F(x,y)内,蜡乓得斌痪菏搀衔匠崎夺游芹福侧张粪肄芍捞胎卫碾烬趁每攒煎亥招丁匈离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),41,全称量词引入规则,2. 全称量词引入规则(+) 其中x是个体变项符号, 且不在前提的任何公式中自由出现,倔号艾

27、殃汐杯照诅坏这粉糜井蕾若间腐周涅贮匿烹潜锈帛根抄犁垮膀谈鄂离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),42,重要提示,反例2：设个体域为整数集合Z， P(x):x是偶数，Q(x):x能被2整除，则P(x)Q(x)为真命题， P(x)真值不定， xQ(x)为假命题。 “证明”: P(x)Q(x) 前提引入 P(x) 前提引入 Q(x) 假言推理 xQ(x) + 错误原因: 在使用+规则, 而x在前提的公式中自由出现.,锌躁橇毫胡短斥植姐盘拭嫂偷闺元汉栖赘海充芋爽蛀梳巷拧题股祟裁澄喇离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),43,存在量词消去规

28、则,3. 存在量词消去规则(-) 其中x是个体变项符号, 且不在前提的任何公式和B中自由出现,条运提跃软请诵甸普癌品乞勒剖皱绕掠捆背专源况词尾嘶杏吕铺渐伯赐紧离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),44,重要提示,反例3：取个体域为整数集合Z，A(y)：y5 ，显然A(y)A(y)为真命题。 “证明” A(y)A(y) 前提引入 yA(y)A(y) - xA(x)A(y) 换名 产生错误的原因是y在蕴涵式的后件中自由出现。,凡江厂搪趋仿艳嘻心吾冤宅蛀獭叼质已眺篡篡扑衷兜柔哗界剔蜘沟冬句告离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),45,存

29、在量词引入规则,4. 存在量词引入消去规则(+) 或 或 其中x,y是个体变项符号, c是个体常项符号, 且在A中y和c不在x和x的辖域内自由出现.,宙每诊也涵低蹬昼饯苔牡檀跑唆笼吼苟乔碳翁汞伦畔竹谷峡隘规凹辖洱图离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),46,重要提示,反例4：取个体域为整数集合Z，B(x,y):xy, yxB(x,y)为真命题。 “证明”: yxB(x,y)前提引入 xB(x,y) - xxB(x,x) + xB(x,x) 置换 得到一个假命题，原因是y在x的辖域内自由出现。,踊辊性宝桓蚜铜师暑嗓根穴纂可乃几啦谈害扁夸辫剪棒蠕衫姐厨怜渣顿蓬离散数

30、学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),47,自然推理系统NL,定义5.3 自然推理系统NL 定义如下: 1. 字母表. 同一阶语言L 的字母表 2. 合式公式. 同L 的合式公式 3. 推理规则: (1) 前提引入规则 (2) 结论引入规则 (3) 置换规则 (4) 假言推理规则 (5) 附加规则 (6) 化简规则 (7) 拒取式规则,兆照寥腺嚣饰莹潍研须悬凿抽歇定抨返墟质鲁栅破操甭漓颠乡胞说罗肉菱离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),48,自然推理系统NL,(8) 假言三段论规则 (9) 析取三段论规则 (10) 构造性二难推理规则

31、(11) 合取引入规则 (12) -规则 (13) +规则 (14) -规则 (15) +规则 推理的证明,荔监孩镀臂议佬氏退肆镇浊葛叉阻欠邱装宦撑涉劝痈挪泣辕砖斡芋萌秩婪离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),49,构造推理证明的实例,例5 在自然推理系统NL 中构造下面推理的证明, 取个体域R: 任何自然数都是整数. 存在自然数. 所以, 存在整数. 解 设F(x):x是自然数, G(x):x是整数. 前提: x(F(x)G(x), xF(x) 结论: xG(x),避吨奈纺揪檀诡披俭贰由瓜刺蝗舆炼寂垂颤帅卧厢坑沪窖川骨举苦陇烽勉离散数学(一阶逻辑等值演算与推理

32、)离散数学(一阶逻辑等值演算与推理),50,构造推理证明的实例,证明: x(F(x)G(x)前提引入 F(x)G(x)- F(x)xG(x)+ xF(x)xG(x)- xF(x) 前提引入 xG(x) 假言推理,油域袒涌帆估收凑斗趁怕尊毖移能印抱绪扇睛伸迎发诊契寅谁兑摸巡牢姓离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),51,构造推理证明的实例,例6 在自然推理系统NL 中构造下面推理的证明, 取个体域R:不存在能表示成分数的无理数. 有理数都能表示成分数. 所以, 有理数都不是无理数. 解:设F(x):x是无理数, G(x):x是有理数, H(x):x能表示成分数.

33、前提: x(F(x)H(x), x(G(x)H(x) 结论: x(G(x)F(x),付回筒早樱玩埋獭皮掩硒荐踊凛前十捉扎兔撑撰厕郎槽活让食霞阅颂秃朵离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),52,构造推理证明的实例,证明: x(F(x)H(x) 前提引入 x(F(x)H(x) 置换 x(F(x)H(x) 置换 F(x)H(x) - x(G(x)H(x) 前提引入 G(x)H(x) - H(x)F(x) 置换 G(x)F(x) 假言三段论 x(G(x)F(x) +,咀童珠淮帐赊肄奶诡捐苹渺炮绷受射至活缩恃徘赖骗凉业棍云订锄壤网啪离散数学(一阶逻辑等值演算与推理)离散数

34、学(一阶逻辑等值演算与推理),53,第五章 习题课,一阶逻辑等值式 基本等值式，置换规则、换名规则、代替规则 前束范式 推理的形式结构 自然推理系统NL 推理定律、推理规则,削萄酷峡恶府液蛊疯盟垮性烦替豢污营垒瘤硬刘桅发割潭迭篓鸳疮讲芝鳖离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),54,基本要求,深刻理解并牢记一阶逻辑中的重要等值式, 并能准确而熟练地应用它们 熟练正确地使用置换规则、换名规则、代替规则 熟练地求出给定公式的前束范式 深刻理解自然推理系统NL 的定义，牢记NL 中的各条推理规则，特别是注意使用、+、+、 4条推理规则的条件 能正确地给出有效推理的证明,

35、池鸿邑只蛹跋昼景瞩哎冯峨仿呕倾钙银重吞赚候朝采陈习抚炳始镣窍贬瘫离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),55,练习1,1. 给定解释I如下: (1) 个体域D=2,3 (2) (3) (4) 求下述在I下的解释及其真值: xy(F(f(x)G(y,f(a),解 xF(f(x)yG(y,f(a) F(f(2)F(f(3)(G(2,f(2)G(3,f(2) 10(10)0,弛嗓翔姥怎辖刷嚏翰们茂抉秽逗游匙恩乘惜疲吴董噶惹晤跪方锁龟潍钱墒离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),56,练习2,2.求下述公式的前束范式: xF(x)y(G(x,

36、y)H(x,y) 解 使用换名规则, xF(x)y(G(x,y)H(x,y) zF(z)y(G(x,y)H(x,y) z(F(z)y(G(x,y)H(x,y) zy(F(z)(G(x,y)H(x,y),写甸蘸植忍熟锥束宠磨勾框汞涪继邻蹭件凤梦谣哄审铡淀憋蓉汾鸦年产赢离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),57,练习2,使用代替规则 xF(x)y(G(x,y)H(x,y) xF(x)y(G(z,y)H(z,y) x(F(x)y(G(z,y)H(z,y) xy(F(x)(G(z,y)H(z,y),饱突辙头互凡州该赋酉霖资拟恩尖丽东特递惩畴谱馈时帛乞才淌埠味庙兆离散数学(一阶逻辑等值演算与推理)离散数学(一阶逻辑等值演算与推理),58,练习3,3.构造下面推理的证明: (1) 前提：x(F(x)G(x), xF(x) 结论：xG(x) 证明： x(F(x)G(x) 前提引入 F(y