消解(归结)原理讲解

解题如下：
（1）取消“→”和“↔”连接词。
(x)(~ (y)P(x, y) ~ (y)(~ Q(x, y) R(x, y)))
（2）把“~”的辖域减少到最多只作用于一 个谓词。
(x)((y) ~ P(x, y) (y)(Q(x, y) ~ R(x, y)))
归结原理
要证明： C1∧C2 => C12，也就是要证明，使C1 和C2为真的解释I，也必使C12为真。
设I是使C1和C2为真的任一解释，若I下的P为真， 从而~P为假。由C2为真的假设可以推出必有 在I下C2’为真，故在I下，由于C12=C1’ ∨C2’ ， 所以C12也为真。若在解释I下P为假，从而由 于假设C1为真，必有C1’为真，故在解释I下 C12=C1’ ∨C2’也必为真。于是我们得到如下定 理：
如果将谓词公式G的Skolem标准型前面的全 称量词全部消去，并用逗号（，）代替合 取符号，便可得到谓词公式G的子句集。 例如在上面的例子中已求得谓词公式G的 Skolem标准型，因而G的子句集S为
S {~ P(x, f (x)) Q(x, g(x)), ~ P(x, f (x)) ~ R(x, g(x))}
不可满足意义下的一致性
例：设有谓词公式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时的GSl=kFolem标准型Gl=P(a)(第一种情况），取a=1，这 导致G与其Skolem标准型（进而与子句集S）不等值的原
（5）全称量词移到左边，由于只有一个全称量 词，已在左边，所以不移。
（6）将母式化为合取范式。
(x)((~ P(x, f (x)) Q(x, g(x))) ((~ P(x, f (x)) ~ R(x, g(x))))
子句与子句集
文字：不含有任何连接词的谓词公式叫原子公式，简称原子，而 原子或原子的否定统称文字。
（x1（) x2（) xn（) x1)M (x1, x2 , , xn )
其中 M (x1, x2, , xn ) 是一个合取范式，称为Skolem 标准形的母式。
将谓词公式G化为Skolem标准型的步骤如下
1消去谓词公式G中蕴涵符（）和双条件符号（↔ ），以 ~A B代替A B，以（A B） （~A ~B）替换A↔ B
无量词约束 元素只是文字的析取 否定符只作用于单个文字 元素间默认为和取 例：{~I(z)R(z), I(A), ~R(x) L(x), ~D(y)}
子句与子句集
由于谓词公式的Skolem标准型的母式已为合 取范式，从而母式的每一个合取项都是一 个子句。也就是说，谓词公式Skolem标准 型的母式是由一些子句的合取组成的。
2 减少否定符（~）的辖域，使否定符号最多只作用到一个 谓词上。
3 重新命名变元，使所有的变元名字均不同，并且自由变元 与约束变元亦不同。
4 消去存在量词。这里分两种情况，一种情况是存在量词不 在全称量词的辖域内，此时，只要用一个新的个体常量替 换该存在量词约束的变元；另一种情况是，存在量词位于 一个或多个全称量词的辖域内，例如：
归结原理
定理：归结式C12是其亲本子句C1和C2的逻 辑结论。
由它可以得出如下的推论： 推论：设C1和C2是子句集S上的子句，C12
是C1和C2归结式。如果把C12加入子句集 S后得到新子句集S1，则S1和S在不可满 足的意义下是等价的。即： S是不可满足的 S1是不可满足的
归结推理过程
由上面的推论以及空子句的不可满足性，可以得 到证明子句集S不可满足性的推理过程如下：
将谓词公式G化为Skolem标准型（续）
（3）变量更名。 (x)((y) ~ P(x, y) (z)(Q(x, z) ~ R(x, z))) （4）消存在量词。因为存在量词和都在辖域内， 属于上述所讲的第二种情况，所以分别用 Skolem函数f(x)和g(x)替换y和z。
(x)((~ P(x, f (x)) (Q(x, g(x)) ~ R(x, g(x))))
(x)(y)(z)(P(x) F( y, z) Q( y, z))
即是一个前束形的范式。优点：量词全部集中在公式的 前面，此部分称作公式的首标，而公式的其余部分 实际上是一个命题演算公式。缺点：杂乱无章，量 词的排列没有一定的规则。
范式
2. 斯克林范式（Skolem） 斯克林范式对前束形范式进行了改进，使得首标
例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)}
中所出现的量词具有一定的规则，即每个存在 量词均在全称量词的前面。如
(x)(y)(z)(P(x) Q( y) F(z))
这是离散数学中有关Skolem范式的定义。在人 工智能的归结推理研究中，Skolem标准形的定 义是，从前束形范式中消去全部存在量词所得 到的公式称为Skolem标准形，它的一般形式是
归结推理规则
设有两个子句：C1=P∨C1’ 和C2=~P∨C2’ P和~P是两个互补文字，则消去互补文字
后得： C12=C1’ ∨C2’ 这一归结过程就是一种推理规则。实际上，
归结推理方法就只有这么一条规则。为 了说明推理规则的正确性，应该证明归 结式C12是C1和C2的逻辑结论，即要证明： C1∧C2 => C12
命题逻辑中的归结原理
互补文字：若P是原子谓词公式或原子命题， 则称P与~P是互补文字。
归结与归结式：设C1与C2式子句中的任意两个 子句，如果C1中的文字L1与C2中的文字L2互补， 则从C1与C2中可以分别消去L1和L2，并将二子 句中余下的部分做析取构成一个新的子句C12 ， 称这一过程为归结，所得到的子句C12称为C1和 C2的归结式，而C1和C2称为C12的亲本子句。
S中的子句变化情况。 （1）~P ∨ Q （2）~Q （3）P （4）~P （1）（2）进行归结 （5）NIL （3）（4）进行归结 由于S中出现了空子句NIL，从而证明了S的不可满足性。
在命题逻辑中，对不可满足的子句集S，
归结原理是完备的。也就是说，如果子
句集S是不可满足的，则必然存在一个从 S到空子句的使用归结推理规则的归结推 理过程；反之，若存在一个从S到空子句 （NIL）使用归结推理规则的归结过程， 则S一定是不可满足的。但是，对于那些 可满足的子句集S，使用归结推理规则将 得不到任何结果。
化子句集的方法（续1）
3, 变量标准化 即：对于不同的约束，对应于不同的变量 (x)A(x) (x)B(x) => (x)A(x) (y)B(y)
4, 消存在量词 (skolem化） 原则：对于一个受存在量词约束的变量，如果他不受 全程量词约束，则该变量用一个常量代替，如果他受 全程量词约束，则该变量用一个函数代替。 (z) (x)(y){[(~P(x) ~Q(x)) R(y)] U(z)}
因是，在谓词公式化为Skolem标准型的过程中，当消 除全称量词左侧的存在量词时，从个体域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的子句集。
谓词公式与子句集
然而，由于谓词公式千变万化，形形色色， 给谓词演算的研究带来一定的困难。为 此，这里先介绍两种谓词演算公式的标 准型，也就是范式；因而对谓词演算的 研究就可以归结为对范式的研究。
范式
1. 前束形范式 一个谓词公式，如果它的所有量词均非否定地出现在公
式的最前面，且它的辖域一直延伸到公式之末，同 时公式中不出现连接词→及↔，这种形式的公式称作 前束形范式。例如公式
=> (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)]
（x1（) x2 )（xn )(y)P( x1, x2 , , xn，y)
将谓词公式G化为Skolem标准型的步骤（续）
此时，变元y实际受前面的变元的约束，需要用 Skolem函数 f (x1, x2 , , xn ) 替换y即可将存在 量词y消去，得到：
（x1（) x2 )（xn )P(x1, x2 , , xn，f ( x1, x2 , , xn ))
（1）对子句集S中的各子句间使用归结推理规则。 （2）将归结所得的归结式放入子句集S中，得到
新子句集S’。 （3）检查子句集S’中是否有空子句（NIL），若
有，则停止推理；否则，转（4） （4）置S:= S’，转（1）
例
证明子句集S={~P ∨ Q，~Q，P}是不可满足的。 证明 按照上述的归结推理过程对S使用归结推理，下面是