《【2018年整理】4.3-1-归结演绎推理》由会员分享，可在线阅读，更多相关《【2018年整理】4.3-1-归结演绎推理（40页珍藏版）》请在金锄头文库上搜索。
1、1第4章 自动动推理2第4章 自动动推理4.1 引言 4.2 自然演绎推理 4.3 归结演绎推理-134.3 归结归结 演绎绎推理-14 归结证明过程是一种反驳程序，即：不是证 明一个公式是有效的(valid)，而是证明公式 之非是不可满足的(dissatisfiable)。这完全是 为了方便，并且不失一般性。 埃尔布朗(Herbrand)(也称海明伦)提出的埃 尔布朗论域和埃尔布朗定理为自动定理证明 奠定了理论基础。鲁宾逊(Robinson)原理使 定理证明的机械化变为现实。4.3 归结演绎推理-15 若欲证明前提条件P可推导出结论Q，即证 明 永真，该问题的证明等价于证明 永假，即 是不可
2、满足的。 4.3 归结演绎推理-16 由于谓词逻辑是命题逻辑的推广，命题逻辑 中的基本等价式和推理规则在谓词逻辑仍可 沿用。但由于谓词逻辑中引入了变量及量词 ，须再增加一些与变量、量词有关的一些定 理和规则，现一并归纳于下:4.3.1 Skolem标准型7 双重否定律(double negation law):(P(x) P(x) 德摩根定律(Mogen law):(P(x)Q(x) P(x) Q(x)(P(x)Q(x) P(x) Q(x)1、谓词演算的基本等价式8 逆否律(inverse-negation law): P(x) Q(x) Q(x) P(x) 分配律(assignment la
3、w):P(x)(Q(x)R(x)(P(x)Q(x)(P(x)R(x) P(x)(Q(x)R(x)(P(x)Q(x)(P(x)R(x)1、谓词演算的基本等价式9 结合律(association law):（P(x)Q(x)R(x)P(x)(Q(x)R(x)（P(x)Q(x)R(x) P(x)(Q(x)R(x) 蕴含等价式(implication law): P(x)Q(x) P(x)Q(x)1、谓词演算的基本等价式10 易名规则(rename law):x P(x) x Q(x)x P(x) y Q(y) 量词转换律(quantifier transform law): x P(x) x P(x
4、) x P(x) x P(x)1、谓词演算的基本等价式11 量词分配律(quantifier assignment law): x (P(x)Q(x) x P(x) x Q(x) x (P(x)Q(x) x P(x) x Q(x) x (P Q(x) P x Q(x) x (P Q(x) P x Q(x)1、谓词演算的基本等价式12 量词交换律(quantifier commutative law): x y(P(x, y) y x(P(x, y) x y(P(x, y) ) y x(P(x, y) x y(P(x, y) ) y x (P(x, y) x y (P(x, y) ) y x (
5、P(x, y)1、谓词演算的基本等价式13 量词辖域变换等价式: xP(x)Q x(P(x)Q) xP(x)Q x(P(x)Q) xP(x)Q x(P(x)Q) xP(x)Q x(P(x)Q) Q中不含变量1、谓词演算的基本等价式14全称量词消去规则: x P(x)P(y) 全称量词引入规则: P(y)x P(x) 存在量词消去规则: xQ(x)Q(c)(c为常量) 存在量词引人规则: Q(c) x Q(x) 2、量词消去及引入规则15有限域量词消去规则:设有限个体域为Dd1， d2，dn x P(x)P(d1)P(d2)，P(dn) x Q(x)Q(d1) Q(d2)，Q(dn)2、量词消去
6、及引入规则163、谓词逻辑中的范式 同一个命题或谓词公式可以用不同的命题或谓 词公式形式来表达，这些公式形式之间是相互 等值的。为了把这些公式规范化，下面讨论公 式范式问题。 所谓范式就是公式的标准形式，公式往往可以 转换为和它等价的范式，以便对它们做一般性 的处理。 方法是：对给定公式中的某子公式用与它“等 价”的一个公式来代替，并且重复该过程直到 得出所需要的形式为止。下面给出一些定义。17范式中的一些定义: 定义4.1 文字(literal)是原子或原子之非。 定义4.2 公式G，当且仅当G有形式 G1Gn (n=1)其中每个Gi都是文字的 析取式。则G称为合取范式(conjunctiv
7、e normal form)3、谓词逻辑中的范式18 定义4.3 公式G称为析取范式(disjunctive normal form)，逻辑公式的标准化(或规范化) ，它是合取子句的析取.当且仅当G有形式 G1Gn(n=1)其中每个Gi都是文字的合 取式。例如: 在命题逻辑中，若P、Q、R是原子，则P、Q、R、 P、 Q、 R都是文字。(P QR) (P Q)是合取范式。(PQ)(PQ R)是析取范式。3、谓词逻辑中的范式19 定理4.1 对任意公式，都有与之等值的合取范式 和析取范式。 可按下述程序使用上一节中的等价式将一个 公式化为合取范式或析取范式。(1) 使用等价式中的连接词化规律消去
8、公式 中的连接词, 。(2) 反复使用双重否定律和德摩根律将 “”移到原子之前。(3) 反复使用分配律和其他定律得出一个标 准型。3、谓词逻辑中的范式20 定义4.4 设F为一谓词公式，如果其中的所有量词均非否定 地出现在公式的最前面，而它们的辖域为整个公式，则称 F为前束范式(prenex normal form)。一般地，前束范式 可以写成:其中 为前缀， 是一个由全称量词或 存在量词组成的量词串， 为母式，它是一个不含任 何量词的谓词公式。4、前束标准型n在一阶逻辑中，为了简化定理证明程序需要引入 所谓的“前束标准型”。21下面是一些前束范式的例子：为了把一个公式化为前束范式，需要对上一
9、节的等 价式扩充，使之包含一阶逻辑特有的等价式对，如 下所示。 4、前束标准型22在上述等价公式对中，F(x)和 H(x)都表示含 未量化变量x的公式，G表示不含未量化变量x的 公式，Q1,Q2 或为 或为。对(3)和(4)，要求z不出现在F(x) 中，并且符 合约束变量的换名原则。 4、前束标准型23使用前面定义的等价式，总可以把一个公式化为 前束标准型。 变换过程如下： (1) 使用等价式中的连接词化归律消去公式中的连接词 、 。 (2) 反复使用双重否定律和德摩根律将“()”移到原 子之前。 (3) 必要时重新命名量化的变量。 (4) 使用量词分配律和等价式，把所有量词都移到整个公 式的
10、最左边以得出一个范式。 4、前束标准型245、Skolem标准化过程Step1: 化成前束范式:Step2: 使用下述方法可以消去前缀中存在的所有量词：令 是 中出现的存在量词 。 Case1: 若在 之前不出现全称量词，则选择一个与M中 出现的所有常量都不相同的新常量c，用c代替M中出现 的所有xr，并且由前缀中删去(Qrxr) 。Case2: 若在 之前出现全称量词 ，则选择一个 与M中出现的任一函数符号都不相同的新m元函数符号f ，用 代替M中的所有xr ，并且由前缀中删去 (Qrxr) 。25例题例4.1 化公式为Skolem标准型。按上述方法删去前缀中的所有存在量词之后得出的 公式称
11、为合式公式的Skolem标准型。替代存在量化 变量的常量c(视为0元函数)和函数f称为Skolem函数 。26在公式中， 的前面没有全称量词， 的前面有全称量词 和 , 在 的前面有全称量词 ， 和 。所以，在 中，用常数a代替x, 用二元函数f(y,z)代替u, 用三元函数g(y,z,v)代替w,去掉前缀中的所有存在量词之后得出Skolem标准型：例题分析27Skolem标准型定理 定理:若G是给定的公式,而相应的子句集为S,则 G是不可满足的当且仅当S是不可满足的 推论：设G=G1 Gn, Si 是 Gi的Skolem标准 型，令S= Si Sn ，则，G是不可满足的当 且仅当S是不可满足
12、的。 P121定理证明284.3.2 子句型 归结证明过程是一种反驳程序，即：不是证明 一个公式是有效的(valid)，而是证明公式之非 是不可满足的(dissatisfiable)。这完全是为了方 便，并且不失一般性。 我们知道，归结推理规则所应用的对象是命题 或谓词合式公式的一种特殊的形式，称为子句 。因此在进行归结之前需要把合式公式化为子 句式。294.3.2 子句型 定义4.5：任何文字的析取式称为子句。例如 PQ， P(x,F(x),y)Q(y)R(f(x)都是子句 。定义4.6：不包含任何文字的子句称为空子句空子句中不包含任何文字，不能被任何解释满足 ，所以空子句是永假的，不可满足
13、的。由子句构成的集合称为子句集。在谓词逻辑中，任何一个谓词公式都可以化成一个 子句集。304.3.2 子句型 n谓词公式化为子句集步骤(1)消去蕴涵符号：利用等价谓词关系消去谓词公 式中的蕴涵符“ ”和双条件符“ ”。(2)减少否定符号的辖域：利用下列等价关系把否 定符号“”移到紧靠谓词的位置上。31(3)变量标准化：重新命名变元名，使不同量词约束 的变元有不同的名字 (4)消去存在量词存在量词不出现在全称量词的辖域内，此 时只要用一个新的个体常量替换该存在量 词的约束变元可消去存在量词存在量词位于一个或多个全称量词的辖域 内，如：4.3.2 子句型 324.3.2 子句型 (5)将公式化为前
14、束形:把全称量词移到公式左边，并使每个量词的辖域 包含这个量词后面的整个部分，所得的公式 称为前束形. (6)把母式化为合取范式:利用等价关系 ，把公 式化为Skolem标准形。Skolem标准形的 一般形式是33(7)消去全称量词与合取词 。 如PQ可表示为子句集:PQ (8)更改变量名，有时称为变量分离标准化。对 变元更名，使不同子句中的变元不同名4.3.2 子句型 34例4.2 将合式公式化为子句形。例题35解：（1）消去蕴涵符号： 这可以利用等价式： 得到： x(P(x)yP(y) P(f(x,y)yQ(x,y) P(y)（2）减少否定符号的辖域，把“ ”移到紧 靠谓词的位置上： 这可以利用下述等价式：例题36得到： x(P(x)yP(y) P(f(x,y)yQ(x,y) P(y) （3）变量标准化：重新命名变元名，使不同量 词约束的变元有不同的名字： x
