AI4-1归结原理专用课件.pptVIP

第4章 归结原理及其应用 1930年Herbrand为定理证明建立了一种重要方法，他的方法奠定了机械定理证明的基础。机械定理证明的主要突破是1965年由J.A.Robinson做出的，他建立了所谓的归结原理，使机械定理证明达到了应用阶段。 4.1 引言 因此，为了证明一组公式蕴涵某个推论，可以采用反证法的思想，即：F1、…Fn、G为公式，G为F1、…Fn的逻辑推论，当且仅当公式（F1∧…∧Fn∧ G）是不可满足的。这样如果公式F1∧…∧Fn是无矛盾的，那么就证明了 G的加入产生了矛盾，所以G就是与F1∧…Fn无矛盾的。 4.1 引言 归结法的本质上就是一种反证法，它是在归结推理规则的基础上实现的。为了证明一个命题P恒真，就证明其反命题 P恒假，即不存在使得 P为真的解释，由于量词，以及嵌套的函数符号，使得谓词公式往往有无穷的指派，不可能一一测试 P是否为真或假。那么如何来解决这个问题呢？幸运的是存在一个域，即Herbrand域，它是一个可数无穷的集合，如果一个公式基于Herbrand解释为假，则就在所有的解释中取假值。 4.1 引言 基于Herbrand域，Herbrand给出了重要的定理，为不可满足的公式判定过程奠定了基础。Robinson给出了用于从不可满足的公式推出F的归结推理规则，使定理机械证明取得了重要的突破，达到了应用的阶段。 4.1 引言 证明的基本思想是： 设F1、…、Fn、G为公式，G为F1、…、Fn的逻辑推论，当且仅当公式（（F1?…?Fn）?G）是有效的 也可以采用反证法的思想： 设F1、…、Fn、G为公式，G为F1、…、Fn的逻辑推论，当且仅当公式（F1?…?Fn ? ?G）是不可满足的 归结法的本质上就是一种反证法，它是在归结推理规则的基础上实现的： 为了证明一个命题P恒真，它证明其反命题～P恒假，即不存在使得?P为真的解释 4.2 命题演算中的归结 4.2.1 归结推理规则 1子句和子句集 一个子句就是一组文字的析取，一个文字或是一个原子（这时也称为正文字），或者是一个原子的否定（这时也称为负文字）,如P、Q、 R都是文字，P∨Q∨R是子句。 4.2 命题演算中的归结 文字是原子或其否定 子句是文字的析取 完备连接符集合： 合取范式（CNF） （L11 ?… ? L1n1) ?… ? (Lm1 ?… ? Lmnm) 析取范式（DNF） （L11 ? … ? L1n1) ? … ? (Lm1 ? … ? Lmnm) 定理： 对任意公式，都有与之等值的合取范式和析取范式 转换方法：一般方法 真值表方法 4.2 命题演算中的归结 定理证明的任务: 由前提A1 ?A2 ?... ?An 推出结论B 即证明:A1 ?A2 ?... ?An?B 永真 转化为证明: A1 ?A2 ?... ?An ? ~B为永假式 归结推理就是:从A1 ?A2 ?... ?An ? ~B出发,使用归结推理规则来找出矛盾,最后证明定理A1 ?A2 ?... ?An?B的成立 4.2 命题演算中的归结 归结方法是一种机械化的,可在计算机上加以实现的推理方法 可认为是一种反向推理形式 提供了一种自动定理证明的方法 4.2化子句集的方法 例：(?z) (?x)(?y){[(P(x) ?Q(x)) ?R(y)] ?U(z)} 1, 消蕴涵符 理论根据：a ?b = ~a ?b (?z) (?x)(?y){[~(P(x) ?Q(x)) ? R(y)] ?U(z)} 2, 移动否定符 理论根据：~(a ?b) = ~a ?~b ~(a ?b) = ~a ?~b ~(?x)P(x)=(?x)~P(x) ~(?x)P(x)=(?x)~P(x) (?z) (?x)(?y){[(~P(x) ?~Q(x)) ? R(y)] ?U(z)} 4.2化子句集的方法 3, 变量标准化 即：对于不同的约束，对应于不同的变量 (?x)A(x) ? (?x)B(x) = (?x)A(x) ? (?y)B(y) 4, 量词左移 (?x)A(x) ? (?y)B(y) = (?x) (?y) {A(x) ? B(y)} 5, 消存在量词 (skolem化） 原则：对于一个受存在量词约束的变量，如果他不受全程量词约束，则该变量用一个常量代替，如果他受全程量词约束，则该变量用一个函数代替。 (?z) (?x)(?y){[(~P(x) ?~Q(x)) ? R(y)] ?U(z)} = (?x) {[(~P(x) ?~