数理逻辑归结法原理上课讲义.ppt

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

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

2、=R，当且仅当Q1…Qn

3、R不可满足证明Q1,…,Qn

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

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

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

7、=R。机械式地证明Ω不可满足是关键问题子句与空子句定义：原子公式及其否定称为文字(literals)；文字的简单析取范式称为子句，不包含文字的子句称为空子句，

8、记为□。例如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。例如，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和Q

9、2的归结子句。例如，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的归结子句。定理：如果子句Q是Q1,Q2的归结子句，则Q1,Q2

10、=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

11、)=1.有σ(q1…qnr1…rm)=1，即σ(Q)=1。证毕反驳定义：设Ω是子句集合，如果子句序列Q1,…,Qn满足如下条件，则称子句序列Q1,…,Qn为子句集合Ω的一个反驳。(1).对于每个1≤k

12、设为Q1,…,Qn是反驳。(1).若QkΩ，Ω

13、=Qk.(2).若Ω

14、=Qi，Ω

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

16、=Qk。因此，Ω

17、=Qk。(3).因为Qn=□，所以有Qn-1和Qk是相反文字，不妨设是q和q。因此，Ω

18、=q，Ω

19、=q。Ω

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

21、不可满足，则有有穷子句集合Ω0，Ω0Ω，使得Ω0是不可满足的。若有穷子句集合Ω0是不可满足的，则Ω0中的子句必出现相反文字。假设有穷子句集合Ω0是不可满足的，且Ω0中的子句不出现相反文字，那么，对于Ω0中子句的每个文字qk，有赋值函数σ使得σ(qk)=1，因此，σ(Ω0)=1，Ω0是可满足的，这样与Ω0是不可满足的相矛盾。设Ω0有n种相反文字，有相反文字q和q，Ω0中的子句分为三类，一类是有文字q的子句，另一类是有文字q的子句，再一类是没有文字q和q的子句Ωq={qPk

22、qPkΩ}，Ωq={qQk

23、qQkΩ}，ΩC=Ω-Ωq

24、-Ωq

25、Ωq

26、=m1，

27、Ωq

28、=m2，

29、ΩC

30、=m3。ΩR={PiQj

31、qPiΩq,qQjΩ