数理逻辑归结法原理课件.ppt
- 【下载声明】
1. 本站全部试题类文档,若标题没写含答案,则无答案;标题注明含答案的文档,主观题也可能无答案。请谨慎下单,一旦售出,不予退换。
2. 本站全部PPT文档均不含视频和音频,PPT中出现的音频或视频标识(或文字)仅表示流程,实际无音频或视频文件。请谨慎下单,一旦售出,不予退换。
3. 本页资料《数理逻辑归结法原理课件.ppt》由用户(三亚风情)主动上传,其收益全归该用户。163文库仅提供信息存储空间,仅对该用户上传内容的表现方式做保护处理,对上传内容本身不做任何修改或编辑。 若此文所含内容侵犯了您的版权或隐私,请立即通知163文库(点击联系客服),我们立即给予删除!
4. 请根据预览情况,自愿下载本文。本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
5. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007及以上版本和PDF阅读器,压缩文件请下载最新的WinRAR软件解压。
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 数理逻辑 归结 原理 课件
- 资源描述:
-
1、计算机学院1计算机学院1主要内容主要内容 机械证明简介机械证明简介 命题逻辑归结法命题逻辑归结法 谓词逻辑归结法谓词逻辑归结法计算机学院2计算机学院2 自动推理早期的工作主要集中在机器定理证明。自动推理早期的工作主要集中在机器定理证明。 机械定理证明的中心问题是寻找判定公式是否是有效的机械定理证明的中心问题是寻找判定公式是否是有效的通用程序。通用程序。 对命题逻辑公式,由于解释的个数是有限的,总可以建对命题逻辑公式,由于解释的个数是有限的,总可以建立一个通用判定程序,使得在有限时间内判定出一个公立一个通用判定程序,使得在有限时间内判定出一个公式是有效的或是无效的。式是有效的或是无效的。 对一阶
2、逻辑公式,其解释的个数通常是任意多个,丘奇对一阶逻辑公式,其解释的个数通常是任意多个,丘奇(A.ChurchA.Church)和图灵()和图灵(A.M.TuringA.M.Turing)在)在19361936年证明了不存年证明了不存在判定公式是否有效的通用程序。在判定公式是否有效的通用程序。如果一阶逻辑公式是有效的,则存在通用程序可以验证它如果一阶逻辑公式是有效的,则存在通用程序可以验证它是有效的是有效的对于无效的公式这种通用程序一般不能终止。对于无效的公式这种通用程序一般不能终止。计算机学院3计算机学院3 19301930年希尔伯特(年希尔伯特(HerbrandHerbrand)为定理证明建
3、立了一种重)为定理证明建立了一种重要方法,他的方法奠定了机械定理证明的基础。要方法,他的方法奠定了机械定理证明的基础。 开创性的工作是赫伯特开创性的工作是赫伯特西蒙(西蒙(H. A. SimonH. A. Simon)和艾伦)和艾伦纽威尔(纽威尔(A. NewelA. Newel)的)的 Logic Theorist Logic Theorist。 机械定理证明的主要突破是机械定理证明的主要突破是19651965年由鲁宾逊(年由鲁宾逊(J.A.RobinsonJ.A.Robinson)做出的,他建立了所谓归结原理,使机械)做出的,他建立了所谓归结原理,使机械定理证明达到了应用阶段。定理证明达到
4、了应用阶段。 归结法推理规则简单归结法推理规则简单, , 而且在逻辑上是完备的而且在逻辑上是完备的, , 因而成为因而成为逻辑式程序设计语言逻辑式程序设计语言PrologProlog的计算模型。的计算模型。计算机学院4计算机学院4主要内容主要内容 机械证明简介机械证明简介 命题逻辑归结法命题逻辑归结法 谓词逻辑归结法谓词逻辑归结法计算机学院5计算机学院5基本原理基本原理 Q Q1 1, ,Q,Qn n|=R|=R,当且仅当,当且仅当Q Q1 1 Q Qn nR R不可满足不可满足 证明证明Q Q1 1, ,Q,Qn n|=R|=R(1). Q(1). Q1 1 Q Qn nR R化为合取范式;
5、化为合取范式;(2). (2). 构建构建 子句集合,子句集合, 为为Q Q1 1 Q Qn nR R合取范合取范式的所有简单析取范式组成集合;式的所有简单析取范式组成集合;(3).(3).若若 不可满足,则不可满足,则Q Q1 1, ,Q,Qn n|=R|=R。计算机学院6计算机学院6机械式方法机械式方法 若证明若证明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计算机学院7子句与空子句子句与空子句 定义:原子公式及其否定称为文字定义:原子公式及其否定称为文字(literals)(literals);文字的简单析取范式称为子句,不包含文字文字的简单析取范式称为子句,不包含文字的子句称为空子句,记为。的子句称为空子句,记为。 例如例如p p、 q q、 r r和和s s都是文字都是文字简单析取式简单析取式p pq qr r s s是子句是子句字字p p、 q q、 r r和和s s因为因为p pq qr r s
7、 s不是简单析取范式,所以不是简单析取范式,所以p pq qr r s s不是子句。不是子句。计算机学院8计算机学院8 定义:设定义:设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计算机学院9归结子句归结子句 定义:设定义:设Q Q1 1,Q,Q2 2是子句,是子句,q q1 1和和q q2 2是相反文字,并且在子句是相反文字,并且在子句Q Q1 1和和Q Q2
8、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 Q1 1和和Q Q2 2的归结子句。的归结子句。 例如,例
9、如,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计算机学院10 定理:如果子句定理:如果子句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 qn n,Q Q2 2= = p p r r1 1 r
10、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计算机学院11反驳反驳 定义:设定义:设 是子句集合,如果子句序列是子句集合,如果子句序列Q Q1 1, ,Q,Qn n满足如下
11、条件,则称子句序列满足如下条件,则称子句序列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计算机学院12 例题:例题:(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, QQ Q Q1 1=
展开阅读全文