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

归结法原理 马殿富北航计算机学院dfma 2012 4 主要内容 机械证明简介命题逻辑归结法谓词逻辑归结法 自动推理早期的工作主要集中在机器定理证明 机械定理证明的中心问题是寻找判定公式是否是有效的通用程序 对命题逻辑公式 由于解释的个数是有限的 总可以建立一个通用判定程序 使得在有限时间内判定出一个公式是有效的或是无效的 对一阶逻辑公式 其解释的个数通常是任意多个 丘奇 A Church 和图灵 A M Turing 在1936年证明了不存在判定公式是否有效的通用程序 如果一阶逻辑公式是有效的 则存在通用程序可以验证它是有效的对于无效的公式这种通用程序一般不能终止 1930年希尔伯特 Herbrand 为定理证明建立了一种重要方法 他的方法奠定了机械定理证明的基础 开创性的工作是赫伯特 西蒙 H A Simon 和艾伦 纽威尔 A Newel 的LogicTheorist 机械定理证明的主要突破是1965年由鲁宾逊 J A Robinson 做出的 他建立了所谓归结原理 使机械定理证明达到了应用阶段 归结法推理规则简单 而且在逻辑上是完备的 因而成为逻辑式程序设计语言Prolog的计算模型 主要内容 机械证明简介命题逻辑归结法谓词逻辑归结法 基本原理 Q1 Qn R 当且仅当Q1 Qn R不可满足证明Q1 Qn R 1 Q1 Qn R化为合取范式 2 构建 子句集合 为Q1 Qn R合取范式的所有简单析取范式组成集合 3 若 不可满足 则Q1 Qn R 机械式方法 若证明Q1 Qn R 只要证明Q1 Qn R不可满足 机械式证明 公式Q1 Qn R的合取范式 合取范式的所有简单析取范式 即 证明 不可满足则有Q1 Qn R 机械式地证明 不可满足是关键问题 子句与空子句 定义 原子公式及其否定称为文字 literals 文字的简单析取范式称为子句 不包含文字的子句称为空子句 记为 例如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和Q2的归结子句 例如 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 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 1 有 q1 qn r1 rm 1 即 Q 1 证毕 反驳 定义 设 是子句集合 如果子句序列Q1 Qn满足如下条件 则称子句序列Q1 Qn为子句集合 的一个反驳 1 对于每个1 k n Qk Qk是Qi和Qj的归结子句 i k j k 2 Qn是 例题 Q R Q Q皮尔斯律证明 因为 Q R Q Q的合取范式Q R Q Q 所以子句集合 Q R Q Q Q1 QQ1 Q2 QQ2 Q3 Q3 Q1 Q Q2 Q 定理 子句集合 是不可满足的当且仅当存在 的反驳 证明 设为Q1 Qn是反驳 1 若Qk Qk 2 若 Qi Qj并且Qk是Qi Qj的归结子句 则Qi Qj Qk 因此 Qk 3 因为Qn 所以有Qn 1和Qk是相反文字 不妨设是q和 q 因此 q q q q 不可满足 又证 设子句集合 是不可满足的 1 不妨设子句集合 不含永真式 因为从 中去掉永真式不改变 的不可满足性 2 若 含有相反文字 不妨设是q 则Q1 qQ1 Q2 qQ2 Q3 因此 Q1 Q2 Q3是反驳 3 根据命题逻辑紧致性定理 若子句集合 不可满足 则有有穷子句集合 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 q Pk q q Qk q Qk C q q q m1 q m2 C m3 R Pi Qj q Pi q q Qj q 1 C R 1有n 1个命题变元 若有r 1并且 r 1 则存在反驳 若 q q C不可满足 则 1 C R不可满足 若 1是可满足的 则有赋值函数 使得 1 1 如果 Pi 1 i 1 m1 那么有 q 0 而其他命题变元r有 r r q Pi 1 其中 q Pi q q Qj 1 其中 q Qj q Rk 1 其中 Rk C因此 若 1是可满足的 则有 使得 0 1 这样就产生了矛盾 所以 1是不可满足的 如果 Pi 0 i m1 则有Pi Qj 1 j 1 m2 因为 1 1 所以有 Pi Qj 1 即 Qj 1 j 1 m2 设 q 1 而其他命题变元r有 r r q Pi 1 其中 q Pi q q Qj 1 其中 q Qi q Rk 1 其中 Rk C若 1是可满足的 则有 使得 0 1 这样就产生了矛盾 所以 1是不可满足的 因此 1有n 1个命题变元并且 1是不可满足的 对于所有的n进行处理获得 n 必有反驳 否则必有 n可满足 进而有 0可满足 证毕 例题 P Q R P Q P R 分配律 P Q R P Q P R P Q R P Q P R P Q P R P P R Q P R P Q P R P P R Q P Q R 因为 P Q R P Q P R 的合取范式 P Q P R P P R Q P Q R 所以子句集合 P P Q P Q P R P R Q R Q1 P QQ1 Q2 P QQ2 Q3 Q3 Q1 P Q Q2 P Q P Q R P Q P R 分配律 例题 P Q R P R Q R 证明 P Q R P R Q R P Q R P R Q R P Q R P Q R因为 P Q R P R Q R 的合取范式 P Q R P Q R所以子句集合 P Q R P Q R Q1 P Q RQ1 Q2 PQ2 Q3 Q RQ3 Q1 P Q2 P Q4 QQ4 Q5 RQ5 Q3 Q Q4 Q Q6 RQ6 Q7 Q7 Q5 R Q6 R 因此P Q R P R Q R 证毕 谢谢