数理逻辑-归结法原理

《数理逻辑-归结法原理》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、归结法原理马殿富北航计算机学院dfma@buaa.edu.cn2012-4主要内容机械证明简介命题逻辑归结法谓词逻辑归结法自动推理早期的工作主要集中在机器定理证明。机械定理证明的中心问题是寻找判定公式是否是有效的通用程序。对命题逻辑公式，由于解释的个数是有限的，总可以建立一个通用判定程序，使得在有限时间内判定出一个公式是有效的或是无效的。对一阶逻辑公式，其解释的个数通常是任意多个，丘奇（A.Church）和图灵（A.M.Turing）在1936年证明了不存在判定公式是否有效的通用程序。如果一阶逻辑公式是有效的，则存在通用程序可以验证它是有效的对于无效的公式这种通用程序一般不能终止。1

2、930年希尔伯特（Herbrand）为定理证明建立了一种重要方法，他的方法奠定了机械定理证明的基础。开创性的工作是赫伯特·西蒙（H.A.Simon）和艾伦·纽威尔（A.Newel）的LogicTheorist。机械定理证明的主要突破是1965年由鲁宾逊（J.A.Robinson）做出的，他建立了所谓归结原理，使机械定理证明达到了应用阶段。归结法推理规则简单,而且在逻辑上是完备的,因而成为逻辑式程序设计语言Prolog的计算模型。主要内容机械证明简介命题逻辑归结法谓词逻辑归结法基本原理Q1,…,Qn

3、=R，当且仅当Q1…QnR不可满足证明Q1,…,Qn

4、=R(1).Q1…Q

5、nR化为合取范式；(2).构建Ω子句集合，Ω为Q1…QnR合取范式的所有简单析取范式组成集合；(3).若Ω不可满足，则Q1,…,Qn

6、=R。机械式方法若证明Q1,…,Qn

7、=R，只要证明Q1…QnR不可满足。机械式证明：公式Q1…QnR的合取范式；合取范式的所有简单析取范式，即Ω；证明Ω不可满足则有Q1,…,Qn

8、=R。机械式地证明Ω不可满足是关键问题子句与空子句定义：原子公式及其否定称为文字(literals)；文字的简单析取范式称为子句，不包含文字的子句称为空子句，记为□。例如p、q、r和s都是文字简单析取式pqrs是子句字p、q、r

9、和s因为pqrs不是简单析取范式，所以pqrs不是子句。定义：设Q是简单析取范式，q是Q的文字，在Q中去掉文字q，记为Q-q。例如，Q是子句pqrs，Q-q是简单析取范式prs。归结子句定义：设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

10、qr，Q2是子句pws，在子句Q1和Q2中没有相反文字出现，子句Q1Q2，即pqrws不是Q1和Q2的归结子句。定理：如果子句Q是Q1,Q2的归结子句，则Q1,Q2

11、=Q证明：设Q1=pq1…qn，Q2=pr1…rm。赋值函数σ(Q1)=1，即σ(pq1…qn)=1，σ(p)σ(q1…qn)=1.赋值函数σ(Q2)=1，即σ(pr1…rm)=1，σ(p)σ(r1…rm)=1.有σ(q1…qnr1…rm)=1，即σ(Q)=1。证毕反驳定义：设Ω是子句集合，如果子句序列Q1,…,Qn满足如下条件，则称子句序列Q1,

12、…,Qn为子句集合Ω的一个反驳。(1).对于每个1≤k

13、=Qk.(2).若Ω

14、=Qi，Ω

15、=Qj并且Qk是Qi,Qj的归结子句，则Qi,Qj

16、=Qk。因此，Ω

17、=Qk。(3).因为Qn=□，所以有

18、Qn-1和Qk是相反文字，不妨设是q和q。因此，Ω

19、=q，Ω

20、=q。Ω

21、=qq，Ω不可满足。又证：设子句集合Ω是不可满足的。(1).不妨设子句集合Ω不含永真式。因为从Ω中去掉永真式不改变Ω的不可满足性。(2).若Ω含有相反文字，不妨设是q，则Q1=qQ1ΩQ2=qQ2ΩQ3=□因此，Q1,Q2,Q3是反驳.(3).根据命题逻辑紧致性定理，若子句集合Ω不可满足，则有有穷子句集合Ω0，Ω0Ω，使得Ω0是不可满足的。若有穷子句集合Ω0是不可满足的