数理逻辑归结法原理

数理逻辑归结法原理第一页，共二十七页，2022年，8月28日主要内容机械证明简介命题逻辑归结法谓词逻辑归结法第二页，共二十七页，2022年，8月28日自动推理早期的工作主要集中在机器定理证明。机械定理证明的中心问题是寻找判定公式是否是有效的通用程序。对命题逻辑公式，由于解释的个数是有限的，总可以建立一个通用判定程序，使得在有限时间内判定出一个公式是有效的或是无效的。对一阶逻辑公式，其解释的个数通常是任意多个，丘奇（A.Church）和图灵（A.M.Turing）在1936年证明了不存在判定公式是否有效的通用程序。如果一阶逻辑公式是有效的，则存在通用程序可以验证它是有效的对于无效的公式这种通用程序一般不能终止。第三页，共二十七页，2022年，8月28日1930年希尔伯特（Herbrand）为定理证明建立了一种重要方法，他的方法奠定了机械定理证明的基础。开创性的工作是赫伯特·西蒙（H.A.Simon）和艾伦·纽威尔（A.Newel）的LogicTheorist。机械定理证明的主要突破是1965年由鲁宾逊（J.A.Robinson）做出的，他建立了所谓归结原理，使机械定理证明达到了应用阶段。归结法推理规则简单,而且在逻辑上是完备的,因而成为逻辑式程序设计语言Prolog的计算模型。第四页，共二十七页，2022年，8月28日主要内容机械证明简介命题逻辑归结法谓词逻辑归结法第五页，共二十七页，2022年，8月28日基本原理Q1,…,Qn|=R，当且仅当Q1…QnR不可满足证明Q1,…,Qn|=R(1).Q1…QnR化为合取范式；(2).构建Ω子句集合，Ω为Q1…QnR合取范式的所有简单析取范式组成集合；(3).若Ω不可满足，则Q1,…,Qn|=R。第六页，共二十七页，2022年，8月28日机械式方法若证明Q1,…,Qn|=R，只要证明Q1…QnR不可满足。机械式证明：公式Q1…QnR的合取范式；合取范式的所有简单析取范式，即Ω；证明Ω不可满足则有Q1,…,Qn|=R。机械式地证明Ω不可满足是关键问题第七页，共二十七页，2022年，8月28日子句与空子句定义：原子公式及其否定称为文字(literals)；文字的简单析取范式称为子句，不包含文字的子句称为空子句，记为□。例如p、q、r和s都是文字简单析取式pqrs是子句字p、q、r和s因为pqrs不是简单析取范式，所以pqrs不是子句。第八页，共二十七页，2022年，8月28日定义：设Q是简单析取范式，q是Q的文字，在Q中去掉文字q，记为Q-q。例如，Q是子句pqrs，Q-q是简单析取范式prs。第九页，共二十七页，2022年，8月28日归结子句定义：设Q1,Q2是子句，q1和q2是相反文字，并且在子句Q1和Q2中出现，称子句(Q1-q1)(Q2-q2)为Q1和Q2的归结子句。例如，Q1是子句pqr，Q2是子句pqws，q和q是相反文字，子句prws是Q1和Q2的归结子句。例如，Q1是子句q，Q2是子句q，q和q是相反文字，子句□是Q1和Q2的归结子句。例如，Q1是子句pqr，Q2是子句pws，在子句Q1和Q2中没有相反文字出现，子句Q1Q2，即pqrws不是Q1和Q2的归结子句。第十页，共二十七页，2022年，8月28日定理：如果子句Q是Q1,Q2的归结子句，则Q1,Q2|=Q证明：设Q1=pq1…qn，Q2=pr1…rm。

赋值函数σ(Q1)=1，即σ(pq1…qn)=1，σ(p)σ(q1…qn)=1.赋值函数σ(Q2)=1，即σ(pr1…rm)=1，σ(p)σ(r1…rm)=1.有σ(q1…qnr1…rm)=1，即σ(Q)=1。证毕第十一页，共二十七页，2022年，8月28日反驳定义：设Ω是子句集合，如果子句序列Q1,…,Qn满足如下条件，则称子句序列Q1,…,Qn为子句集合Ω的一个反驳。(1).对于每个1≤k<n，QkΩQk是Qi和Qj的归结子句，i<k，j<k。(2).Qn是□。第十二页，共二十七页，2022年，8月28日例题：(QR)Q├Q皮尔斯律证明：因为((QR)Q)Q的合取范式Q(RQ)Q，所以子句集合Ω={Q,RQ,Q}Q1=QQ1ΩQ2=QQ2ΩQ3=□Q3=(Q1-Q)(Q2-Q)第十三页，共二十七页，2022年，8月28日定理：子句集合Ω是不可满足的当且仅当存在Ω的反驳。证明：设为Q1,…,Qn是反驳。(1).若QkΩ，Ω|=Qk.(2).若Ω|=Qi，Ω|=Qj并且Qk是Qi,Qj的归结子句，则Qi,Qj|=Qk。因此，Ω|=Qk。(3).因为Qn=□，所以有Qn-1和Qk是相反文字，不妨设是q和q。因此，Ω|=q，Ω|=q。Ω|=qq，Ω不可满足。第十四页，共二十七页，2022年，8月28日又证：设子句集合Ω是不可满足的。(1).不妨设子句集合Ω不含永真式。因为从Ω中去掉永真式不改变Ω的不可满足性。(2).若Ω含有相反文字，不妨设是q，则Q1=qQ1ΩQ2=qQ2ΩQ3=□因此，Q1,Q2,Q3是反驳.第十五页，共二十七页，2022年，8月28日(3).根据命题逻辑紧致性定理，若子句集合Ω不可满足，则有有穷子句集合Ω0，Ω0Ω，使得Ω0是不可满足的。第十六页，共二十七页，2022年，8月28日若有穷子句集合Ω0是不可满足的，则Ω0中的子句必出现相反文字。假设有穷子句集合Ω0是不可满足的，且Ω0中的子句不出现相反文字，那么，对于Ω0中子句的每个文字qk，有赋值函数σ使得σ(qk)=1，因此，σ(Ω0)=1，Ω0是可满足的，这样与Ω0是不可满足的相矛盾。第十七页，共二十七页，2022年，8月28日设Ω0有n种相反文字，有相反文字q和q，Ω0中的子句分为三类，一类是有文字q的子句，另一类是有文字q的子句，再一类是没有文字q和q的子句第十八页，共二十七页，2022年，8月28日Ωq={qPk|qPkΩ}，Ωq={qQk|qQkΩ}，ΩC=Ω-Ωq-Ωq|Ωq|=m1，|Ωq|=m2，|ΩC|=m3。ΩR={Pi

Qj|qPiΩq,qQjΩq}Ω1=ΩCΩRΩ1有n-1个命题变元。若有rΩ1并且rΩ1，则存在反驳。第十九页，共二十七页，2022年，8月28日若Ωq

Ωq

ΩC

不可满足，则Ω1=ΩCΩR不可满足。若Ω1是可满足的，则有赋值函数σ，使得σ(Ω1)=1。如果σ(Pi)=1，i=1,...,m1，那么有σ'(q)=0，而其他命题变元r有σ'(r)=σ(r)。σ'(qPi)=1，其中，qPiΩqσ'(qQj)=1，其中，qQjΩqσ'(Rk)=1，其中，RkΩC因此，若Ω1是可满足的，则有σ'，使得σ'(Ω0)=1，这样就产生了矛盾，所以，Ω1是不可满足的。第二十页，共二十七页，2022年，8月28日如果σ(Pi)=0，i≤m1，则有PiQjΩ1，j=1,…,m2。因为σ(Ω1)=1，所以有σ(PiQj)=1，即σ(Qj)=1，j=1,…,m2。设σ'(q)=1，而其他命题变元r有σ'(r)=σ(r)。σ'(qPi)=1，其中，qPiΩqσ'(qQj)=1，其中，qQiΩqσ'(Rk)=1，其中，RkΩC若Ω1是可满足的，则有σ'，使得σ'(Ω0)=1，这样就产生了矛盾，所以，Ω1是不可满足的。第二十一页，共二十七页，2022年，8月28日因此，Ω1有n-1个命题变元并且Ω1是不可满足的。对于所有的n进行处理获得Ωn，必有反驳，否则必有Ωn可满足，进而有Ω0可满足。证毕第二十二页，共二十七页，2022年，8月28日例题：P(QR)├(PQ)(PR)分配律(P(QR))((PQ)(PR))(P(QR))((PQ)(PR))(PQ)(PR))(P(PR))(Q(PR))(PQ)(PR)P(P

R)(QP)(QR)因为(P(QR))((PQ)(PR))的合取范式(PQ)(PR)P(P

R)(QP)(QR)所以子句集合 Ω={P,PQ,PQ,PR,PR,QR}。第二十三页，共二十七页，2022年，8月28日Q1=PQQ1ΩQ2=PQQ2ΩQ3=□Q3=(Q1-P-Q)(Q2-P-Q)P(QR)├(PQ)(PR)分配律第二十四页，共二十七页，2022年，8月28日例题：PQR├(PR)(QR)证明：(PQR)((PR)(QR))((PQ)R)(PRQR)(PQR)PQR因为(PQR)((PR)(QR))的合取范式(PQR)PQR所以子句集合 Ω={P,Q,R,PQR}第二十五页，共二十七页，2022年，8月28日Q1=PQRQ1ΩQ2=PQ2ΩQ3=QR