数理逻辑归结法原理课件.ppt

1、计算机学院1计算机学院1主要内容主要内容 机械证明简介机械证明简介 命题逻辑归结法命题逻辑归结法 谓词逻辑归结法谓词逻辑归结法计算机学院2计算机学院2 自动推理早期的工作主要集中在机器定理证明。自动推理早期的工作主要集中在机器定理证明。 机械定理证明的中心问题是寻找判定公式是否是有效的机械定理证明的中心问题是寻找判定公式是否是有效的通用程序。通用程序。 对命题逻辑公式，由于解释的个数是有限的，总可以建对命题逻辑公式，由于解释的个数是有限的，总可以建立一个通用判定程序，使得在有限时间内判定出一个公立一个通用判定程序，使得在有限时间内判定出一个公式是有效的或是无效的。式是有效的或是无效的。 对一阶

2、逻辑公式，其解释的个数通常是任意多个，丘奇对一阶逻辑公式，其解释的个数通常是任意多个，丘奇（A.ChurchA.Church）和图灵（）和图灵（A.M.TuringA.M.Turing）在）在19361936年证明了不存年证明了不存在判定公式是否有效的通用程序。在判定公式是否有效的通用程序。如果一阶逻辑公式是有效的，则存在通用程序可以验证它如果一阶逻辑公式是有效的，则存在通用程序可以验证它是有效的是有效的对于无效的公式这种通用程序一般不能终止。对于无效的公式这种通用程序一般不能终止。计算机学院3计算机学院3 19301930年希尔伯特（年希尔伯特（HerbrandHerbrand）为定理证明建

3、立了一种重）为定理证明建立了一种重要方法，他的方法奠定了机械定理证明的基础。要方法，他的方法奠定了机械定理证明的基础。 开创性的工作是赫伯特开创性的工作是赫伯特西蒙（西蒙（H. A. SimonH. A. Simon）和艾伦）和艾伦纽威尔（纽威尔（A. NewelA. Newel）的）的 Logic Theorist Logic Theorist。 机械定理证明的主要突破是机械定理证明的主要突破是19651965年由鲁宾逊（年由鲁宾逊（J.A.RobinsonJ.A.Robinson）做出的，他建立了所谓归结原理，使机械）做出的，他建立了所谓归结原理，使机械定理证明达到了应用阶段。定理证明达到

4、了应用阶段。 归结法推理规则简单归结法推理规则简单, , 而且在逻辑上是完备的而且在逻辑上是完备的, , 因而成为因而成为逻辑式程序设计语言逻辑式程序设计语言PrologProlog的计算模型。的计算模型。计算机学院4计算机学院4主要内容主要内容 机械证明简介机械证明简介 命题逻辑归结法命题逻辑归结法 谓词逻辑归结法谓词逻辑归结法计算机学院5计算机学院5基本原理基本原理 Q Q1 1, ,Q,Qn n|=R|=R，当且仅当，当且仅当Q Q1 1 Q Qn nR R不可满足不可满足 证明证明Q Q1 1, ,Q,Qn n|=R|=R(1). Q(1). Q1 1 Q Qn nR R化为合取范式；

5、化为合取范式；(2). (2). 构建构建 子句集合，子句集合， 为为Q Q1 1 Q Qn nR R合取范合取范式的所有简单析取范式组成集合；式的所有简单析取范式组成集合；(3).(3).若若 不可满足，则不可满足，则Q Q1 1, ,Q,Qn n|=R|=R。计算机学院6计算机学院6机械式方法机械式方法 若证明若证明Q Q1 1, ,Q,Qn n|=R|=R，只要证明，只要证明Q Q1 1 Q Qn nR R不可满足。不可满足。 机械式证明：机械式证明：公式公式Q Q1 1 Q Qn nR R的合取范式；的合取范式；合取范式的所有简单析取范式，即合取范式的所有简单析取范式，即 ；证明证明

6、不可满足不可满足 则有则有Q Q1 1, ,Q,Qn n|=R|=R。 机械式地证明机械式地证明 不可满足是关键问题不可满足是关键问题计算机学院7计算机学院7子句与空子句子句与空子句 定义：原子公式及其否定称为文字定义：原子公式及其否定称为文字(literals)(literals)；文字的简单析取范式称为子句，不包含文字文字的简单析取范式称为子句，不包含文字的子句称为空子句，记为。的子句称为空子句，记为。 例如例如p p、 q q、 r r和和s s都是文字都是文字简单析取式简单析取式p pq qr r s s是子句是子句字字p p、 q q、 r r和和s s因为因为p pq qr r s

7、 s不是简单析取范式，所以不是简单析取范式，所以p pq qr r s s不是子句。不是子句。计算机学院8计算机学院8 定义：设定义：设Q Q是简单析取范式，是简单析取范式，q q是是Q Q的文字，在的文字，在Q Q中中去掉文字去掉文字q q，记为，记为Q-qQ-q。 例如，例如，Q Q是子句是子句p pq qr r s s，Q - Q - q q是简单析取范式是简单析取范式p p r r s s。计算机学院9计算机学院9归结子句归结子句 定义：设定义：设Q Q1 1,Q,Q2 2是子句，是子句，q q1 1和和q q2 2是相反文字，并且在子句是相反文字，并且在子句Q Q1 1和和Q Q2

8、2中出现，称子句中出现，称子句(Q(Q1 1-q-q1 1) ) (Q(Q2 2-q-q2 2) )为为Q Q1 1和和Q Q2 2的归结的归结子句。子句。 例如，例如，Q Q1 1是子句是子句p pq qr r，Q Q2 2是子句是子句p p q q w w s s， q q和和q q是相反文字，子句是相反文字，子句p pr r w w s s是是Q Q1 1和和Q Q2 2的归结子句。的归结子句。 例如，例如，Q Q1 1是子句是子句 q q，Q Q2 2是子句是子句q q， q q和和q q是相反文字，是相反文字，子句是子句是Q Q1 1和和Q Q2 2的归结子句。的归结子句。 例如，例

9、如，Q Q1 1是子句是子句p pq qr r，Q Q2 2是子句是子句p p w w s s，在子句，在子句Q Q1 1 和和Q Q2 2中没有相反文字出现，子句中没有相反文字出现，子句Q Q1 1 Q Q2 2，即，即p pq qr r w w s s不是不是Q Q1 1和和Q Q2 2的归结子句。的归结子句。计算机学院10计算机学院10 定理：如果子句定理：如果子句Q Q是是Q Q1 1, Q, Q2 2的归结子句，则的归结子句，则Q Q1 1, Q, Q2 2|=Q|=Q 证明：证明： 设设Q Q1 1=p=p q q1 1 q qn n，Q Q2 2= = p p r r1 1 r

10、rm m。 赋值函数赋值函数(Q(Q1 1)=1)=1，即，即(p(p q q1 1 q qn n)=1)=1， (p)(p) (q (q1 1 q qn n)=1.)=1. 赋值函数赋值函数(Q(Q2 2)=1)=1，即，即( ( p p r r1 1 r rm m)=1)=1， (p)(p) (r (r1 1 r rm m)=1.)=1. 有有(q(q1 1 q qn n r r1 1 r rm m)=1)=1，即，即(Q)=1(Q)=1。 证毕证毕计算机学院11计算机学院11反驳反驳 定义：设定义：设 是子句集合，如果子句序列是子句集合，如果子句序列Q Q1 1, ,Q,Qn n满足如下

11、条件，则称子句序列满足如下条件，则称子句序列Q Q1 1, ,Q,Qn n为子句集合为子句集合 的一个反驳。的一个反驳。 (1).(1).对于每个对于每个1 1k knn，Q Qk k Q Qk k是是Q Qi i和和Q Qj j的归结子句，的归结子句，ikik，jkjk。 (2). (2). Q Qn n是。是。计算机学院12计算机学院12 例题：例题：(Q(QR)R)Q QQ Q 皮尔斯律皮尔斯律 证明：证明： 因为因为(Q(QR)R)Q)Q)Q Q的合取范式的合取范式Q Q ( ( R R Q)Q)Q Q，所以，所以子句集合子句集合=Q, =Q, R R Q, Q, QQ Q Q1 1=

12、 Q Q= Q Q1 1 Q Q2 2= = Q QQ Q2 2 Q Q3 3= = Q Q3 3= (Q= (Q1 1-Q) -Q) (Q (Q2 2- - Q)Q)计算机学院13计算机学院13 定理：子句集合定理：子句集合 是不可满足的当且仅当存在是不可满足的当且仅当存在 的反的反驳。驳。 证明：设为证明：设为Q Q1 1, ,Q,Qn n是反驳。是反驳。 (1).(1).若若Q Qk k ，|=Q|=Qk. k. (2).(2).若若|=Q|=Qi i，|=Q|=Qj j并且并且Q Qk k是是Q Qi i, Q, Qj j的归结子句，则的归结子句，则Q Qi i, Q, Qj j|=Q

13、|=Qk k。因此，。因此，|=Q|=Qk k。 (3).(3).因为因为Q Qn n= =，所以有，所以有Q Qn-1n-1和和Q Qk k是相反文字，不妨设是相反文字，不妨设是是q q和和 q q。 因此，因此，|=q|=q，|=|= q q。|=q|=qq q， 不可满足。不可满足。计算机学院14计算机学院14 又证：设子句集合又证：设子句集合 是不可满足的。是不可满足的。 (1).(1).不妨设子句集合不妨设子句集合 不含永真式。因为从不含永真式。因为从 中去掉永真中去掉永真式不改变式不改变 的不可满足性。的不可满足性。 (2).(2).若若 含有相反文字，不妨设是含有相反文字，不妨设

14、是q q，则，则 Q Q1 1=q Q=q Q1 1 Q Q2 2= = q Qq Q2 2 Q Q3 3= = 因此，因此，Q Q1 1, Q, Q2 2,Q,Q3 3是反驳是反驳. .计算机学院15计算机学院15 (3).(3).根据命题逻辑紧致性定理，若子句集合根据命题逻辑紧致性定理，若子句集合 不可满足，则有有穷子句集合不可满足，则有有穷子句集合 0 0， 0 0 ，使，使得得 0 0是不可满足的。是不可满足的。计算机学院16计算机学院16 若有穷子句集合若有穷子句集合 0 0是不可满足的，则是不可满足的，则 0 0中的子句必中的子句必出现相反文字。出现相反文字。 假设有穷子句集合假设

15、有穷子句集合 0 0是不可满足的，且是不可满足的，且 0 0中的子句中的子句不出现相反文字，那么，对于不出现相反文字，那么，对于 0 0中子句的每个文字中子句的每个文字q qk k，有赋值函数，有赋值函数 使得使得(q(qk k)=1)=1，因此，因此，(0 0)=1)=1， 0 0是是可满足的，这样与可满足的，这样与 0 0是不可满足的相矛盾。是不可满足的相矛盾。计算机学院17计算机学院17 设设 0 0有有n n种相反文字，有相反文字种相反文字，有相反文字q q和和 q q， 0 0中的子句分为三类，中的子句分为三类，一类是有文字一类是有文字q q的子句，的子句，另一类是有文字另一类是有文

16、字 q q的子句，的子句，再一类是没有文字再一类是没有文字q q和和 q q的子句的子句计算机学院18计算机学院18 q q = q = q P Pk k| q| q P Pk k ， q q = = q q Q Qk k| | q q Q Qk k ， C C=-=-q q- q q |q q |=m |=m1 1，| q q |=m |=m2 2，|C C|=m|=m3 3。 R R= P= Pi i Q Qj j| q| q P Pi i q q, , q q Q Qj j q q 1 1 = =C C R R 1 1有有n-1n-1个命题变元。个命题变元。 若有若有r r 1 1并且并

17、且 r r 1 1，则存在反驳。，则存在反驳。计算机学院19计算机学院19 若若 q q q q C C 不可满足，则不可满足，则 1 1 = =C C R R不可满足。不可满足。 若若 1 1是可满足的，则有赋值函数是可满足的，则有赋值函数 ，使得，使得(1 1)=1)=1。 如果如果(P(Pi i)=1)=1，i i=1,.,m=1,.,m1 1，那么有，那么有(q)=0(q)=0，而其他命题变元，而其他命题变元r r有有(r)=(r)(r)=(r)。 (q(q P Pi i)=1)=1，其中，其中，q q P Pi i q q ( q q Q Qj j)=1)=1，其中，其中， q q

18、Q Qj j q q (R(Rk k)=1)=1，其中，其中，R Rk k C C 因此，若因此，若 1 1是可满足的，则有是可满足的，则有 ，使得，使得(0 0)=1)=1，这样就，这样就产生了矛盾，所以，产生了矛盾，所以， 1 1是不可满足的。是不可满足的。计算机学院20计算机学院20 如果如果(P(Pi i)=0)=0，i im m1 1，则有，则有P Pi i Q Qj j 1 1，j=1,j=1,m,m2 2。 因为因为(1 1)=1)=1，所以有，所以有(P(Pi i Q Qj j)=1)=1，即，即(Q(Qj j)=1)=1，j=1,j=1,m,m2 2。 设设(q)=1(q)=

19、1，而其他命题变元，而其他命题变元r r有有(r)=(r)(r)=(r)。 (q(q P Pi i)=1)=1，其中，其中，q q P Pi i q q ( q q Q Qj j)=1)=1，其中，其中， q q Q Qi i q q (R(Rk k)=1)=1，其中，其中，R Rk k C C 若若 1 1是可满足的，则有是可满足的，则有 ，使得，使得(0 0)=1)=1，这样就产生了，这样就产生了矛盾，所以，矛盾，所以， 1 1是不可满足的。是不可满足的。计算机学院21计算机学院21 因此，因此， 1 1有有n-1n-1个命题变元并且个命题变元并且 1 1是不可满足的。是不可满足的。 对于

20、所有的对于所有的n n进行处理获得进行处理获得 n n，必有反驳，否则必有，必有反驳，否则必有 n n可满足，进而有可满足，进而有 0 0可满足。可满足。 证毕证毕计算机学院22计算机学院22 例题：例题：P P(Q(Q R)R) (P (PQ)Q) (P (PR) R) 分配律分配律 (P(P(Q(Q R) R) (P (PQ)Q) (P (PR)R) ( ( P P (Q(Q R) R) (P (PQ) Q) (P (PR)R) ( ( P P Q) Q) ( ( P P R)R) ( P( P (P (PR) R) ( ( Q Q (P (PR)R) ( ( P P Q) Q) ( (

21、P P R)R) P P ( P( P R) R) ( ( Q Q P) P) ( ( Q QR)R) 因为因为(P(P(Q(Q R) R) (P (PQ)Q) (P (PR)R)的合取范式的合取范式 ( ( P P Q) Q) ( ( P P R)R) P P ( P( P R) R) ( ( Q Q P) P) ( ( Q QR) R) 所以子句集合所以子句集合 = P,P= P,PQ, Q, P P Q, PQ, PR ,R , P P R , R , Q QRR。计算机学院23计算机学院23 Q Q1 1= P= PQ QQ Q1 1 Q Q2 2= = P P Q QQ Q2 2 Q

22、 Q3 3= = Q Q3 3= (Q= (Q1 1-P-P- Q) Q) (Q (Q2 2- - P-Q)P-Q) P P(Q(Q R)R) (P (PQ) Q) (P (PR) R) 分配律分配律计算机学院24计算机学院24 例题：例题：P P Q QR R(P(PR) R) (Q (QR)R) 证明：证明： (P(P Q QR) R) (P(PR) R) (Q (QR)R) ( ( ( P( P Q) Q) R) R) ( ( P P R RQ Q R)R) ( ( P PQ Q R) R) P P Q QR R 因为因为(P(P Q QR)R)(P(PR)R) (Q(QR)R)的合取范

23、式的合取范式( ( P PQ Q R) R) P P Q QR R 所以子句集合所以子句集合=P,Q, =P,Q, R ,R , P PQ Q R R 计算机学院25计算机学院25 Q Q1 1= = P PQ Q R QR Q1 1 Q Q2 2=P Q=P Q2 2 Q Q3 3= = Q Q R QR Q3 3= (Q= (Q1 1- - P) P) (Q (Q2 2-P)-P) Q Q4 4=Q Q=Q Q4 4 Q Q5 5=R Q=R Q5 5= (Q= (Q3 3- - Q) Q) (Q (Q4 4-Q)-Q) Q Q6 6= = R QR Q6 6 Q Q7 7= = Q Q7 7= (Q= (Q5 5-R) -R) (Q (Q6 6- - R)R) 因此因此P P Q QR R(P(PR) R) (Q (QR)R) 证毕证毕