数理逻辑归结法原理幻灯片.ppt
《数理逻辑归结法原理幻灯片.ppt》由会员分享,可在线阅读,更多相关《数理逻辑归结法原理幻灯片.ppt(27页珍藏版)》请在淘文阁 - 分享文档赚钱的网站上搜索。
1、数理逻辑归结法原理数理逻辑归结法原理第1页,共27页,编辑于2022年,星期六主要内容主要内容机械证明简介机械证明简介命题逻辑归结法命题逻辑归结法谓词逻辑归结法谓词逻辑归结法第2页,共27页,编辑于2022年,星期六自动推理早期的工作主要集中在机器定理证明。自动推理早期的工作主要集中在机器定理证明。机械定理证明的中心问题是寻找判定公式是否是有效的通用程序。机械定理证明的中心问题是寻找判定公式是否是有效的通用程序。对命题逻辑公式,由于解释的个数是有限的,总可以建立对命题逻辑公式,由于解释的个数是有限的,总可以建立一个通用判定程序,使得在有限时间内判定出一个公式是一个通用判定程序,使得在有限时间内
2、判定出一个公式是有效的或是无效的。有效的或是无效的。对一阶逻辑公式,其解释的个数通常是任意多个,丘奇对一阶逻辑公式,其解释的个数通常是任意多个,丘奇(A.ChurchA.Church)和图灵()和图灵(A.M.TuringA.M.Turing)在)在19361936年证明了不存在判定公年证明了不存在判定公式是否有效的通用程序。式是否有效的通用程序。如果一阶逻辑公式是有效的,则存在通用程序可以验证它是有效的如果一阶逻辑公式是有效的,则存在通用程序可以验证它是有效的对于无效的公式这种通用程序一般不能终止。对于无效的公式这种通用程序一般不能终止。第3页,共27页,编辑于2022年,星期六193019
3、30年希尔伯特(年希尔伯特(HerbrandHerbrand)为定理证明建立了一种重要)为定理证明建立了一种重要方法,他的方法奠定了机械定理证明的基础。方法,他的方法奠定了机械定理证明的基础。开创性的工作是赫伯特开创性的工作是赫伯特西蒙(西蒙(H.A.SimonH.A.Simon)和艾伦)和艾伦纽威纽威尔(尔(A.NewelA.Newel)的)的 Logic Theorist Logic Theorist。机械定理证明的主要突破是机械定理证明的主要突破是19651965年由鲁宾逊年由鲁宾逊(J.A.RobinsonJ.A.Robinson)做出的,他建立了所谓归结原理,使机械)做出的,他建立了
4、所谓归结原理,使机械定理证明达到了应用阶段。定理证明达到了应用阶段。归结法推理规则简单归结法推理规则简单,而且在逻辑上是完备的而且在逻辑上是完备的,因而成为逻辑式程因而成为逻辑式程序设计语言序设计语言PrologProlog的计算模型。的计算模型。第4页,共27页,编辑于2022年,星期六主要内容主要内容机械证明简介机械证明简介命题逻辑归结法命题逻辑归结法谓词逻辑归结法谓词逻辑归结法第5页,共27页,编辑于2022年,星期六基本原理基本原理Q Q1 1,Q,Qn n|=R|=R,当且仅当,当且仅当Q Q1 1 Q Qn nR R不可满足不可满足证明证明Q Q1 1,Q,Qn n|=R|=R(1
5、).Q(1).Q1 1 Q Qn nR R化为合取范式;化为合取范式;(2).(2).构建构建 子句集合,子句集合,为为Q Q1 1 Q Qn nR R合取范式的所合取范式的所有简单析取范式组成集合;有简单析取范式组成集合;(3).(3).若若 不可满足,则不可满足,则Q Q1 1,Q,Qn n|=R|=R。第6页,共27页,编辑于2022年,星期六机械式方法机械式方法若证明若证明Q Q1 1,Q,Qn n|=R|=R,只要证明,只要证明Q Q1 1 Q Qn nR R不可不可满足。满足。机械式证明:机械式证明:公式公式Q Q1 1 Q Qn nR R的合取范式;的合取范式;合取范式的所有简单
6、析取范式,即合取范式的所有简单析取范式,即;证明证明 不可满足不可满足则有则有Q Q1 1,Q,Qn n|=R|=R。机械式地证明机械式地证明 不可满足是关键问题不可满足是关键问题第7页,共27页,编辑于2022年,星期六子句与空子句子句与空子句定义:原子公式及其否定称为文字定义:原子公式及其否定称为文字(literals)(literals);文字;文字的简单析取范式称为子句,不包含文字的子句称的简单析取范式称为子句,不包含文字的子句称为空子句,记为为空子句,记为。例如例如p p、q q、r r和和s s都是文字都是文字简单析取式简单析取式p pq qr r s s是子句是子句字字p p、q
7、 q、r r和和s s因为因为p pq qr r s s不是简单析取范式,所以不是简单析取范式,所以p pq qr r s s不是子句。不是子句。第8页,共27页,编辑于2022年,星期六定义:设定义:设Q Q是简单析取范式,是简单析取范式,q q是是Q Q的文字,在的文字,在Q Q中去掉中去掉文字文字q q,记为,记为Q-qQ-q。例如,例如,Q Q是子句是子句p pq qr r s s,Q-Q-q q是简单析取范式是简单析取范式p p r r s s。第9页,共27页,编辑于2022年,星期六归结子句归结子句定义:设定义:设Q Q1 1,Q,Q2 2是子句,是子句,q q1 1和和q q2
8、 2是相反文字,并且在子句是相反文字,并且在子句Q Q1 1和和Q Q2 2中出现,称子句中出现,称子句(Q(Q1 1-q-q1 1)(Q(Q2 2-q-q2 2)为为Q Q1 1和和Q Q2 2的归结子句。的归结子句。例如,例如,Q Q1 1是子句是子句p pq qr r,Q Q2 2是子句是子句p p q q w w s s,q q和和q q是相反是相反文字,子句文字,子句p pr r w w s s是是Q Q1 1和和Q Q2 2的归结子句。的归结子句。例如,例如,Q Q1 1是子句是子句 q q,Q Q2 2是子句是子句q q,q q和和q q是相反文字,子句是相反文字,子句是是Q Q
9、1 1和和Q Q2 2的归结子句。的归结子句。例如,例如,Q Q1 1是子句是子句p pq qr r,Q Q2 2是子句是子句p p w w s s,在子句,在子句Q Q1 1 和和Q Q2 2中没有相反文字出现,子句中没有相反文字出现,子句Q Q1 1 Q Q2 2,即,即p pq qr r w w s s不是不是Q Q1 1和和Q Q2 2的归结子句。的归结子句。第10页,共27页,编辑于2022年,星期六定理:如果子句定理:如果子句Q Q是是Q Q1 1,Q,Q2 2的归结子句,则的归结子句,则Q Q1 1,Q,Q2 2|=Q|=Q证明:证明:设设Q Q1 1=p=p q q1 1 q
10、qn n,Q Q2 2=p p r r1 1 r rm m。赋值函数赋值函数(Q(Q1 1)=1)=1,即,即(p(p q q1 1 q qn n)=1)=1,(p)(p)(q(q1 1 q qn n)=1.)=1.赋值函数赋值函数(Q(Q2 2)=1)=1,即,即(p p r r1 1 r rm m)=1)=1,(p)(p)(r(r1 1 r rm m)=1.)=1.有有(q(q1 1 q qn n r r1 1 r rm m)=1)=1,即,即(Q)=1(Q)=1。证毕证毕第11页,共27页,编辑于2022年,星期六反驳反驳定义:设定义:设 是子句集合,如果子句序列是子句集合,如果子句序列
11、Q Q1 1,Q,Qn n满满足如下条件,则称子句序列足如下条件,则称子句序列Q Q1 1,Q,Qn n为子句集合为子句集合 的一个反驳。的一个反驳。(1).(1).对于每个对于每个1 1k knn,Q Qk k Q Qk k是是Q Qi i和和Q Qj j的归结子句,的归结子句,ikik,jkjk。(2).(2).Q Qn n是是。第12页,共27页,编辑于2022年,星期六例题:例题:(Q(QR)R)Q QQ Q 皮尔斯律皮尔斯律证明:证明:因为因为(Q(QR)R)Q)Q)Q Q的合取范式的合取范式Q Q(R R Q)Q)Q Q,所以子句,所以子句集合集合=Q,=Q,R R Q,Q,QQQ
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 数理逻辑 归结 原理 幻灯片
限制150内