《数理逻辑-归结法原理》由会员分享，可在线阅读，更多相关《数理逻辑-归结法原理（27页珍藏版）》请在金锄头文库上搜索。
1、归结法原理马殿富 北航计算机学院 2012-4计算机学院2计算机学院2主要内容 机械证明简介 命题逻辑归结法 谓词逻辑归结法计算机学院3计算机学院3 自动推理早期的工作主要集中在机器定理证明。 机械定理证明的中心问题是寻找判定公式是否是有效的 通用程序。 对命题逻辑公式，由于解释的个数是有限的，总可以建 立一个通用判定程序，使得在有限时间内判定出一个公 式是有效的或是无效的。 对一阶逻辑公式，其解释的个数通常是任意多个，丘奇 （A.Church）和图灵（A.M.Turing）在1936年证明了不存 在判定公式是否有效的通用程序。 如果一阶逻辑公式是有效的，则存在通用程序可以验证它 是有效的
2、对于无效的公式这种通用程序一般不能终止。计算机学院4计算机学院4 1930年希尔伯特（Herbrand）为定理证明建立了一种重 要方法，他的方法奠定了机械定理证明的基础。 开创性的工作是赫伯特西蒙（H. A. Simon）和艾伦 纽威尔（A. Newel）的 Logic Theorist。 机械定理证明的主要突破是1965年由鲁宾逊（ J.A.Robinson）做出的，他建立了所谓归结原理，使机械 定理证明达到了应用阶段。 归结法推理规则简单, 而且在逻辑上是完备的, 因而成为 逻辑式程序设计语言Prolog的计算模型。计算机学院5计算机学院5主要内容 机械证明简介 命题逻辑归结法 谓词逻辑归
3、结法计算机学院6计算机学院6基本原理 Q1,Qn|=R，当且仅当Q1QnR不可满足 证明Q1,Qn|=R (1). Q1QnR化为合取范式； (2). 构建子句集合，为Q1QnR合取范式 的所有简单析取范式组成集合； (3).若不可满足，则Q1,Qn|=R。计算机学院7计算机学院7机械式方法 若证明Q1,Qn|=R，只要证明Q1QnR 不可满足。 机械式证明： 公式Q1QnR的合取范式； 合取范式的所有简单析取范式，即； 证明不可满足 则有Q1,Qn|=R。 机械式地证明不可满足是关键问题计算机学院8计算机学院8子句与空子句 定义：原子公式及其否定称为文字(literals)； 文字的简单析取
4、范式称为子句，不包含文字 的子句称为空子句，记为。 例如 p、q、r和s都是文字 简单析取式pqrs是子句 字p、q、r和s 因为pqrs不是简单析取范式，所以 pqrs不是子句。计算机学院9计算机学院9 定义：设Q是简单析取范式，q是Q的文字，在Q中 去掉文字q，记为Q-q。 例如，Q是子句pqrs，Q - q是简单析取范式 p rs。计算机学院10计算机学院10归结子句 定义：设Q1,Q2是子句，q1和q2是相反文字，并且在子句 Q1和Q2中出现，称子句(Q1-q1)(Q2-q2)为Q1和Q2的归结 子句。 例如，Q1是子句pqr，Q2是子句pqws，q和q 是相反文字，子句prws是Q1
5、和Q2的归结子句。 例如，Q1是子句q，Q2是子句q，q和q是相反文字， 子句是Q1和Q2的归结子句。 例如，Q1是子句pqr，Q2是子句pws，在子句Q1 和Q2中没有相反文字出现，子句Q1Q2，即 pqrws不是Q1和Q2的归结子句。计算机学院11计算机学院11 定理：如果子句Q是Q1, Q2的归结子句，则Q1, Q2|=Q 证明： 设Q1=pq1qn，Q2=pr1rm。 赋值函数(Q1)=1，即(pq1qn)=1， (p) (q1qn)=1. 赋值函数(Q2)=1，即(pr1rm)=1， (p) (r1rm)=1. 有(q1qn r1rm)=1，即(Q)=1。 证毕计算机学院12计算机学
6、院12反驳 定义：设是子句集合，如果子句序列 Q1,Qn满足如下条件，则称子句序列 Q1,Qn为子句集合的一个反驳。 (1).对于每个1kn，Qk Qk是Qi和Qj的归结子句，ik，jk。 (2). Qn是。计算机学院13计算机学院13 例题：(QR)QQ 皮尔斯律 证明： 因为(QR)Q)Q的合取范式Q(RQ)Q，所以 子句集合=Q, RQ, Q Q1= Q Q1 Q2= Q Q2 Q3= Q3= (Q1-Q) (Q2-Q)计算机学院14计算机学院14 定理：子句集合是不可满足的当且仅当存在的反 驳。 证明：设为Q1,Qn是反驳。 (1).若Qk，|=Qk. (2).若|=Qi，|=Qj并且
7、Qk是Qi, Qj的归结子句，则 Qi, Qj|=Qk。因此，|=Qk。 (3).因为Qn=，所以有Qn-1和Qk是相反文字，不妨设 是q和q。 因此，|=q，|=q。|=qq，不可满足。计算机学院15计算机学院15 又证：设子句集合是不可满足的。 (1).不妨设子句集合不含永真式。因为从中去掉永真 式不改变的不可满足性。 (2).若含有相反文字，不妨设是q，则 Q1=q Q1 Q2=q Q2 Q3= 因此，Q1, Q2,Q3是反驳.计算机学院16计算机学院16 (3).根据命题逻辑紧致性定理，若子句集合 不可满足，则有有穷子句集合0，0，使 得0是不可满足的。计算机学院17计算机学院17 若
8、有穷子句集合0是不可满足的，则0中的子句必 出现相反文字。 假设有穷子句集合0是不可满足的，且0中的子句 不出现相反文字，那么，对于0中子句的每个文字 qk，有赋值函数使得(qk)=1，因此，(0)=1，0是 可满足的，这样与0是不可满足的相矛盾。计算机学院18计算机学院18 设0有n种相反文字，有相反文字q和q ，0中的子句分为三类， 一类是有文字q的子句， 另一类是有文字q的子句， 再一类是没有文字q和q的子句计算机学院19计算机学院19 q = qPk| qPk，q =qQk| qQk， C=-q-q |q |=m1，|q |=m2，|C|=m3。 R= Pi Qj| qPiq, qQj
9、q 1 =CR 1有n-1个命题变元。 若有r1并且r1，则存在反驳。计算机学院20计算机学院20 若q q C 不可满足，则1 =CR不可满足。 若1是可满足的，则有赋值函数，使得(1)=1。 如果(Pi)=1，i=1,.,m1，那么有(q)=0，而其他命题变元 r有(r)=(r)。 (qPi)=1，其中，qPiq (qQj)=1，其中，qQjq (Rk)=1，其中，RkC 因此，若1是可满足的，则有，使得(0)=1，这样就 产生了矛盾，所以，1是不可满足的。计算机学院21计算机学院21 如果(Pi)=0，im1，则有Pi Qj1，j=1,m2。 因为(1)=1，所以有(Pi Qj)=1，即
10、(Qj)=1，j=1,m2 。 设(q)=1，而其他命题变元r有(r)=(r)。 (qPi)=1，其中，qPiq (qQj)=1，其中，qQiq (Rk)=1，其中，RkC 若1是可满足的，则有，使得(0)=1，这样就产生了 矛盾，所以，1是不可满足的。计算机学院22计算机学院22 因此，1有n-1个命题变元并且1是不可满足的。 对于所有的n进行处理获得n，必有反驳，否则必有n 可满足，进而有0可满足。 证毕计算机学院23计算机学院23 例题：P(QR) (PQ) (PR) 分配律 (P(QR) (PQ) (PR) (P(QR) (PQ) (PR) (PQ) (PR)( P (PR) (Q (
11、PR) (PQ) (PR)P ( P R) (Q P)( QR) 因为(P(QR) (PQ) (PR)的合取范式 (PQ) (PR)P ( P R) (Q P)( QR) 所以子句集合 = P,PQ, PQ, PR ,PR , QR。计算机学院24计算机学院24 Q1= PQ Q1 Q2=PQ Q2 Q3= Q3= (Q1-P-Q) (Q2-P-Q) P(QR) (PQ) (PR) 分配律计算机学院25计算机学院25 例题：PQR(PR) (QR) 证明： (PQR) (PR) (QR) ( PQ) R) (PRQR) (PQR) PQR 因为(PQR)(PR)(QR)的合取范式 (PQR) PQR 所以子句集合 =P,Q, R ,PQR 计算机学院26计算机学院26 Q1=PQR Q1 Q2=P Q2 Q3=QR Q3= (Q1-P) (Q2-P) Q4=Q Q4 Q5=R Q5= (Q3-Q) (Q4-Q) Q6=R Q6 Q7= Q7= (Q5-R) (Q6-R) 因此PQR(PR) (QR) 证毕
