数理逻辑-归结法原理.ppt

该【数理逻辑-归结法原理 】是由【fanluqian】上传分享，文档一共【27】页，该文档可以免费在线阅读，需要了解更多关于【数理逻辑-归结法原理 】的内容，可以使用淘豆网的站内搜索功能，选择自己适合的文档，以下文字是截取该文章内的部分文字，如需要获得完整电子版，请下载此文档到您的设备，方便您编辑和打印。归结法原理
马殿富
北航计算机学院
2012-4
202X
202X
CONTENTS
主要内容
01
Part 01
机械证明简介
03
Part 03
谓词逻辑归结法
02
Part 02
命题逻辑归结法
自动推理早期的工作主要集中在机器定理证明。
机械定理证明的中心问题是寻找判定公式是否是有效的通用程序。
对命题逻辑公式，由于解释的个数是有限的，总可以建立一个通用判定程序，使得在有限时间内判定出一个公式是有效的或是无效的。
对一阶逻辑公式，其解释的个数通常是任意多个，丘奇（）和图灵（）在1936年证明了不存在判定公式是否有效的通用程序。
如果一阶逻辑公式是有效的，则存在通用程序可以验证它是有效的
对于无效的公式这种通用程序一般不能终止。
04
03
01
02
1930年希尔伯特（Herbrand）为定理证明建立了一种重要方法，他的方法奠定了机械定理证明的基础。
开创性的工作是赫伯特·西蒙（H. A. Simon）和艾伦·纽威尔（A. Newel）的 Logic Theorist。
机械定理证明的主要突破是1965年由鲁宾逊（）做出的，他建立了所谓归结原理，使机械定理证明达到了应用阶段。
归结法推理规则简单, 而且在逻辑上是完备的, 因而成为逻辑式程序设计语言Prolog的计算模型。
主要内容
机械证明简介
01
命题逻辑归结法
02
谓词逻辑归结法
03
Q1,…,Qn|=R，当且仅当Q1…QnR不可满足
证明Q1,…,Qn|=R
Q1…QnR化为合取范式；
构建Ω子句集合，Ω为Q1…QnR合取范式的所有简单析取范式组成集合；
若Ω不可满足，则Q1,…,Qn|=R。
若证明Q1,…,Qn|=R，只要证明Q1…QnR不可满足。
机械式证明：
公式Q1…QnR的合取范式；
合取范式的所有简单析取范式，即Ω；
证明Ω不可满足
则有Q1,…,Qn|=R。
机械式地证明Ω不可满足是关键问题
子句与空子句
定义：原子公式及其否定称为文字(literals)；文字的简单析取范式称为子句，不包含文字的子句称为空子句，记为□。
例如
p、q、r和s都是文字
简单析取式pqrs是子句
字p、q、r和s
因为pqrs不是简单析取范式，所以pqrs不是子句。
定义：设Q是简单析取范式，q是Q的文字，在Q中去掉文字q，记为Q-q。
01
例如，Q是子句pqrs，Q - q是简单析取范式p rs。
02
归结子句
定义：设Q1,Q2是子句，q1和q2是相反文字，并且在子句Q1和Q2中出现，称子句(Q1-q1)(Q2-q2)为Q1和Q2的归结子句。
例如，Q1是子句pqr，Q2是子句pqws，q和q是相反文字，子句prws是Q1和Q2的归结子句。
例如，Q1是子句q，Q2是子句q，q和q是相反文字，子句□是Q1和Q2的归结子句。
例如，Q1是子句pqr，Q2是子句pws，在子句Q1 和Q2中没有相反文字出现，子句Q1Q2，即pqrws不是Q1和Q2的归结子句。