《消解(归结)原理》由会员分享，可在线阅读，更多相关《消解(归结)原理（56页珍藏版）》请在金锄头文库上搜索。
1、消解（归结）原理,归结推理,归结推理是一种定理证明方法，1965年由Robinson提出，从理论上解决了定理证明问题。对于定理证明问题，如果用一阶谓词逻辑表示的话，就是要求对前提P和结论Q证明PQ是永真的。然而要证明这个谓词公式的永真性，必须对所有个体域上的每一个解释进行验证，这是极其困难的。为了化简问题，我们考虑反证法，即我们先否定逻辑结论Q，再由否定后的逻辑结论Q及前提条件P出发推出矛盾即可，也就是说，只要证明PQ是不可满足的即可。,谓词公式与子句集,然而，由于谓词公式千变万化，形形色色，给谓词演算的研究带来一定的困难。为此，这里先介绍两种谓词演算公式的标准型，也就是范式；因而对谓词演算的
2、研究就可以归结为对范式的研究。,范式,1. 前束形范式 一个谓词公式，如果它的所有量词均非否定地出现在公式的最前面，且它的辖域一直延伸到公式之末，同时公式中不出现连接词及，这种形式的公式称作前束形范式。例如公式 即是一个前束形的范式。优点：量词全部集中在公式的前面，此部分称作公式的首标，而公式的其余部分实际上是一个命题演算公式。缺点：杂乱无章，量词的排列没有一定的规则。,范式,2. 斯克林范式（Skolem） 斯克林范式对前束形范式进行了改进，使得首标中所出现的量词具有一定的规则，即每个存在量词均在全称量词的前面。如 这是离散数学中有关Skolem范式的定义。在人工智能的归结推理研究中，Sko
3、lem标准形的定义是，从前束形范式中消去全部存在量词所得到的公式称为Skolem标准形，它的一般形式是 其中 是一个合取范式，称为Skolem标准形的母式。,将谓词公式G化为Skolem标准型的步骤如下,1消去谓词公式G中蕴涵符（）和双条件符号（ ），以A B代替A B，以（A B） （A B）替换A B 2 减少否定符（）的辖域，使否定符号最多只作用到一个谓词上。 3 重新命名变元，使所有的变元名字均不同，并且自由变元与约束变元亦不同。 4 消去存在量词。这里分两种情况，一种情况是存在量词不在全称量词的辖域内，此时，只要用一个新的个体常量替换该存在量词约束的变元；另一种情况是，存在量词位于一
4、个或多个全称量词的辖域内，例如：,将谓词公式G化为Skolem标准型的步骤（续）,此时，变元y实际受前面的变元的约束，需要用Skolem函数 替换y即可将存在量词y消去，得到： 5 把全称量词移到公式的左边，并使每个量词的辖域包括这个量词后面公式的整个部分。 6 母式化为合取范式：任何母式都可以写成由一些谓词公式和谓词公式否定的析取的有限集组成的合取。,将谓词公式G化为Skolem标准型,例：将以下谓词公式化为Skolem标准型。 解 按照将谓词公式化为Skolem标准型的步骤解题如下： （1）取消“”和“”连接词。 （2）把“”的辖域减少到最多只作用于一个谓词。,将谓词公式G化为Skolem
5、标准型（续）,（3）变量更名。 （4）消存在量词。因为存在量词和都在辖域内，属于上述所讲的第二种情况，所以分别用Skolem函数f(x)和g(x)替换y和z。 （5）全称量词移到左边，由于只有一个全称量词，已在左边，所以不移。 （6）将母式化为合取范式。,子句与子句集,文字：不含有任何连接词的谓词公式叫原子公式，简称原子，而原子或原子的否定统称文字。 子句：就是由一些文字组成的析取式。如：P(x) Q(x,y), P(x,c) R(x,y,f(x)都是子句。 空子句：不包含任何文字的子句称为空子句，记为NIL。由于空子句不包含任何有任何文字，它不能被任何解释满足，所以空子句是永假的，是不可满足
6、的。 子句集：由子句构成的集合称为子句集。 无量词约束 元素只是文字的析取 否定符只作用于单个文字 元素间默认为和取 例：I(z)R(z), I(A), R(x) L(x), D(y),子句与子句集,由于谓词公式的Skolem标准型的母式已为合取范式，从而母式的每一个合取项都是一个子句。也就是说，谓词公式Skolem标准型的母式是由一些子句的合取组成的。 如果将谓词公式G的Skolem标准型前面的全称量词全部消去，并用逗号（，）代替合取符号，便可得到谓词公式G的子句集。例如在上面的例子中已求得谓词公式G的Skolem标准型，因而G的子句集S为,例2 化子句集的方法,例：(z) (x)(y)(P
7、(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),化子句集的方法（续1）,3, 变量标准化 即：对于不同的约束，对应于不同的变量 (x)A(x) (x)B(x) = (x)A(x) (y)B(y) 4, 消存在量词 (skolem化） 原则：对于一个受存在量词约束的变量，如果他不受全程量词约束，则该变
8、量用一个常量代替，如果他受全程量词约束，则该变量用一个函数代替。 (z) (x)(y)(P(x) Q(x) R(y) U(z) = (x) (P(x) Q(x) R(f(x) U(a) 5, 量词左移 (x)A(x) (y)B(y) = (x) (y) A(x) B(y),化子句集的方法（续2）,6, 化为合取范式 即(ab) (cd) (ef)的形式 (x)(P(x) Q(x) R(f(x)U(a) = (x)(P(x) Q(x) R(f(x)U(a) = (x)P(x) R(f(x)U(a) Q(x) R(f(x)U(a) 7, 隐去全程量词，并用逗号代替合取符号 P(x) R(f(x)U
9、(a), Q(x) R(f(x)U(a),不可满足意义下的一致性,公式G与其子句集并不等值，但它们在不可满足的意义下是一致的。 定理3-2：若S是合式公式G的子句集，则G是不可满足的充要条件是S不可满足。,不可满足意义下的一致性,例：设有谓词公式G= (x)P(x)，说明G与Skolem标准型并不等值。 设G的个体域为D=1,2，此时G=P(1) P(2). 设解释I：P(1)=F,P(2)=T,则在这一解释下G为T。 而G的Skolem标准型Gl=P(a)(第一种情况），取a=1，这时Gl=F 导致G与其Skolem标准型（进而与子句集S）不等值的原因是，在谓词公式化为Skolem标准型的过
10、程中，当消除全称量词左侧的存在量词时，从个体域D中选定的某一个个体a。而存在量词具有“或”的含义，只要个体域D中一个个体使G为真，侧G取值就为T。Skolem标准型只是G的一个特例。,不可满足意义下的一致性,当P= P 1 P 2 P n ,若设P的子句集为S p ，P i的子句集为S i，一般情况下S p不等于S 1 S 2 S n，而要复杂得多，但在不可满足的意义下是一致的。这样对S p的讨论就可由S 1 S 2 S n来代替。为了方便也称S 1 S 2 S n是P的子句集。,消解（归结）原理,子句集中各子句间的关系是合取的关系，因此，只要有一个子句是不可满足的，则子句集是不可满足的。另外
11、，我们在前面已经指出，空子句是不可满足的，所以只要子句集中包含一个空子句，则此子句集就一定是不可满足的。Robinson的归结原理正是基于这一认识提出来的，其基本思想是：检查子句集S中是否有空子句，若有，则表明S是不可满足的；若没有，就在子句集中选择合适的子句对其进行归结推理，如果能推出空子句，则说明子句集S是不可满足的。,命题逻辑中的归结原理,互补文字：若P是原子谓词公式或原子命题，则称P与P是互补文字。 归结与归结式：设C1与C2式子句中的任意两个子句，如果C1中的文字L1与C2中的文字L2互补，则从C1与C2中可以分别消去L1和L2，并将二子句中余下的部分做析取构成一个新的子句C12 ，
12、称这一过程为归结，所得到的子句C12称为C1和C2的归结式，而C1和C2称为C12的亲本子句。,归结推理规则,设有两个子句：C1=PC1 和C2=PC2 P和P是两个互补文字，则消去互补文字后得： C12=C1 C2 这一归结过程就是一种推理规则。实际上，归结推理方法就只有这么一条规则。为了说明推理规则的正确性，应该证明归结式C12是C1和C2的逻辑结论，即要证明： C1C2 = C12,归结原理,要证明： C1C2 = C12，也就是要证明，使C1和C2为真的解释I，也必使C12为真。 设I是使C1和C2为真的任一解释，若I下的P为真，从而P为假。由C2为真的假设可以推出必有在I下C2为真，
13、故在I下，由于C12=C1 C2 ，所以C12也为真。若在解释I下P为假，从而由于假设C1为真，必有C1为真，故在解释I下C12=C1 C2也必为真。于是我们得到如下定理：,归结原理,定理：归结式C12是其亲本子句C1和C2的逻辑结论。 由它可以得出如下的推论： 推论：设C1和C2是子句集S上的子句，C12是C1和C2归结式。如果把C12加入子句集S后得到新子句集S1，则S1和S在不可满足的意义下是等价的。即： S是不可满足的 S1是不可满足的,归结推理过程,由上面的推论以及空子句的不可满足性，可以得到证明子句集S不可满足性的推理过程如下： （1）对子句集S中的各子句间使用归结推理规则。 （2
14、）将归结所得的归结式放入子句集S中，得到新子句集S。 （3）检查子句集S中是否有空子句（NIL），若有，则停止推理；否则，转（4） （4）置S:= S，转（1）,例,证明子句集S=P Q，Q，P是不可满足的。 证明 按照上述的归结推理过程对S使用归结推理，下面是S中的子句变化情况。 （1）P Q （2）Q （3）P （4）P （1）（2）进行归结 （5）NIL （3）（4）进行归结 由于S中出现了空子句NIL，从而证明了S的不可满足性。,在命题逻辑中，对不可满足的子句集S，归结原理是完备的。也就是说，如果子句集S是不可满足的，则必然存在一个从S到空子句的使用归结推理规则的归结推理过程；反之，若
15、存在一个从S到空子句（NIL）使用归结推理规则的归结过程，则S一定是不可满足的。但是，对于那些可满足的子句集S，使用归结推理规则将得不到任何结果。,一阶谓词逻辑中的归结原理,在一阶谓词逻辑中，由于子句中含有变元，所以不能像命题逻辑中那样可以直接消去互补文字进行子句归结。而是首先使用置换与合一的思想，对子句中的某些变元进行合一置换，对置换后的新子句再次使用归结规则。,例如假设有如下两个子句： C1=P(x) Q(x) C2=P(a) T(z) 由于P(x) 与P(a)不同，从而不是互补文字，不能对C1和C2直接进行归结。作如下合一置换：=a/x， 是最一般的置换。对两个子句分别进行置换： C1 =P(a) Q(a) C2 =P(a) T(z) 再对它们进行归结，消去P(a)与P(a)，得到如下归结式： Q(a) T(z),定义 设C1和C2是两个没有相同变元的子句， L1和L2分别是C1和C2的文字，如果L1和L2有mgu ，则把 C12 =( C1 L1 ) ( C1 L1 ) 称作子句C
