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

归结法原理 马殿富 北航计算机学院 2012-4 计算机学院 2计算机学院 2 主要内容 机械证明简介 命题逻辑归结法 谓词逻辑归结法 计算机学院 3计算机学院 3 自动推理早期的工作主要集中在机器定理证明。 机械定理证明的中心问题是寻找判定公式是否是有效的 通用程序。 对命题逻辑公式，由于解释的个数是有限的，总可以建 立一个通用判定程序，使得在有限时间内判定出一个公 式是有效的或是无效的。 对一阶逻辑公式，其解释的个数通常是任意多个，丘奇 （A.Church）和图灵（A.M.Turing）在1936年证明了不存 在判定公式是否有效的通用程序。 如果一阶逻辑公式是有效的，则存在通用程序可以验证它 是有效的 对于无效的公式这种通用程序一般不能终止。 计算机学院 4计算机学院 4 1930年希尔伯特（Herbrand）为定理证明建立了一种重 要方法，他的方法奠定了机械定理证明的基础。 开创性的工作是赫伯特西蒙（H. A. Simon）和艾伦 纽威尔（A. Newel）的 Logic Theorist。 机械定理证明的主要突破是1965年由鲁宾逊（ J.A.Robinson）做出的，他建立了所谓归结原理，使机械 定理证明达到了应用阶段。 归结法推理规则简单, 而且在逻辑上是完备的, 因而成为 逻辑式程序设计语言Prolog的计算模型。 计算机学院 5计算机学院 5 主要内容 机械证明简介 命题逻辑归结法 谓词逻辑归结法 计算机学院 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)； 文字的简单析取范式称为子句，不包含文字 的子句称为空子句，记为。 例如 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和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计算机学院 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并且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 若有穷子句集合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, qQjq 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，即(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 (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)