消解(归结)原理

S {~ P( x, f ( x)) Q( x, g ( x)), ~ P( x, f ( x)) ~ R( x, g ( x))}
例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)}
归结原理
要证明： 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’也必为真。于是我们得到如下 定理：
不可满足意义下的一致性
当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的子句集。
归结原理
定理：归结式C12是其亲本子句C1和C2的逻 辑结论。 由它可以得出如下的推论： 推论：设C1和C2是子句集S上的子句，C12 是C1和C2归结式。如果把C12加入子句集 S后得到新子句集S1，则S1和S在不可满 足的意义下是等价的。即： S是不可满足的 S1是不可满足的
归结推理过程
(x)(y )(z )(P( x) Q( y ) F ( z ))
这是离散数学中有关Skolem范式的定义。在人 工智能的归结推理研究中，Skolem标准形的定 义是，从前束形范式中消去全部存在量词所得 到的公式称为Skolem标准形，它的一般形式是
（x1（ ) x2（ ) xn（ ) x1 ) M ( x1 , x2 ,, xn )
由上面的推论以及空子句的不可满足性，可以得 到证明子句集S不可满足性的推理过程如下： （1）对子句集S中的各子句间使用归结推理规则。 （2）将归结所得的归结式放入子句集S中，得到 新子句集S’。 （3）检查子句集S’中是否有空子句（NIL），若 有，则停止推理；否则，转（4） （4）置S:= S’，转（1）
消解（归结）原理
子句集中各子句间的关系是合取的关系，因此， 只要有一个子句是不可满足的，则子句集是不 可满足的。另外，我们在前面已经指出，空子 句是不可满足的，所以只要子句集中包含一个 空子句，则此子句集就一定是不可满足的。 Robinson的归结原理正是基于这一认识提出来 的，其基本思想是：检查子句集S中是否有空 子句，若有，则表明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)} => (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)]}
消解（归结）原理
归结推理

归结推理是一种定理证明方法，1965年由 Robinson提出，从理论上解决了定理证明问题。 对于定理证明问题，如果用一阶谓词逻辑表示 的话，就是要求对前提P和结论Q证明P→Q是 永真的。然而要证明这个谓词公式的永真性， 必须对所有个体域上的每一个解释进行验证， 这是极其困难的。为了化简问题，我们考虑反 证法，即我们先否定逻辑结论Q，再由否定后 的逻辑结论~Q及前提条件P出发推出矛盾即可， 也就是说，只要证明P∧~Q是不可满足的即可。

无量词约束 元素只是文字的析取 否定符只作用于单个文字 元素间默认为和取 例：{~I(z)R(z), I(A), ~R(x) L(x), ~D(y)}
子句与子句集
由于谓词公式的Skolem标准型的母式已为合 取范式，从而母式的每一个合取项都是一 个子句。也就是说，谓词公式Skolem标准 型的母式是由一些子句的合取组成的。 如果将谓词公式G的Skolem标准型前面的全 称量词全部消去，并用逗号（，）代替合 取符号，便可得到谓词公式G的子句集。 例如在上面的例子中已求得谓词公式G的 Skolem标准型，因而G的子句集S为
解 按照将谓词公式化为Skolem标准型的步 骤解题如下： （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 )))
例：设有谓词公式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标准型的过程中，当消 除全称量词左侧的存在量词时，从个体域D中选定的某 一个个体a。而存在量词具有“或”的含义，只要个体 域D中一个个体使G为真，侧G取值就为T。Skolem标 准型只是G的一个特例。
其中 M ( x1 , x2 ,, xn ) 是一个合取范式，称为Skolem 标准形的母式。
将谓词公式G化为Skolem标准型的步骤如下
1消去谓词公式G中蕴涵符（）和双条件符号（↔ ），以 ~A B代替A B，以（A B） （~A ~B）替换A↔ B 2 减少否定符（~）的辖域，使否定符号最多只作用到一个 谓词上。 3 重新命名变元，使所有的变元名字均不同，并且自由变元 与约束变元亦不同。 4 消去存在量词。这里分两种情况，一种情况是存在量词不 在全称量词的辖域内，此时，只要用一个新的个体常量替 换该存在量词约束的变元；另一种情况是，存在量词位于 一个或多个全称量词的辖域内，例如：
5 把全称量词移到公式的左边，并使每个量词的 辖域包括这个量词后面公式的整个部分。 6 母式化为合取范式：任何母式都可以写成由一 些谓词公式和谓词公式否定的析取的有限集组 成的合取。
将谓词公式G化为Skolem标准型
例：将以下谓词公式化为Skolem标准型。
G (x)((y ) P( x, y ) ~ (y )(Q( x, y ) R( x, y )))
(x)(y )(z )(P( x) F ( y, z ) Q( y, z ))
即是一个前束形的范式。优点：量词全部集中在公式的 前面，此部分称作公式的首标，而公式的其余部分 实际上是一个命题演算公式。缺点：杂乱无章，量 词的排列没有一定的规则。
范式
2. 斯克林范式（Skolem） 斯克林范式对前束形范式进行了改进，使得首标 中所出现的量词具有一定的规则，即每个存在 量词均在全称量词的前面。如
归结推理规则
设有两个子句：C1=P∨C1’ 和C2=~P∨C2’ P和~P是两个互补文字，则消去互补文字 后得： C12=C1’ ∨C2’ 这一归结过程就是一种推理规则。实际上， 归结推理方法就只有这么一条规则。为 了说明推理规则的正确性，应该证明归 结式C12是C1和C2的逻辑结论，即要证明： C1∧C2 => C12
(x)((~ P( x, f ( x)) (Q( x, g ( x)) ~ R( x, g ( x))))
（5）全称量词移到左边，由于只有一个全称量 词，已在左边，所以不移。 （6）将母式化为合取范式。
(x)((~ P( x, f ( x)) Q( x, g ( x))) ((~ P( x, f ( x)) ~ R( x, g ( x))))
子句与子句集



文字：不含有任何连接词的谓词公式叫原子公式，简称原子，而 原子或原子的否定统称文字。 子句：就是由一些文字组成的析取式。如：P(x) ~Q(x,y), ~P(x,c) R(x,y,f(x))都是子句。 空子句：不包含任何文字的子句称为空子句，记为NIL。由于空 子句不包含任何有任何文字，它不能被任何解释满足，所以空子 句是永假的，是不可满足的。 子句集：由子句构成的集合称为子句集。
（x1（ ) x2 ) （xn )(y )P( x1 , x2 ,, xn，y)
将谓词公式G化为Skolem标准型的步骤（续）
此时，变元y实际受前面的变元的约束，需要用 Skolem函数 f ( x1 , x2 ,, xn ) 替换y即可将存在 量词y消去，得到：