消解归结原理讲解课件.ppt

消解（归结）原理归结推理n归结推理是一种定理证明方法，1965年由Robinson提出，从理论上解决了定理证明问题对于定理证明问题，如果用一阶谓词逻辑表示的话，就是要求对前提P和结论Q证明P→Q是永真的然而要证明这个谓词公式的永真性，必须对所有个体域上的每一个解释进行验证，这是极其困难的为了化简问题，我们考虑反证法，即我们先否定逻辑结论Q，再由否定后的逻辑结论~Q及前提条件P出发推出矛盾即可，也就是说，只要证明P∧~Q是不可满足的即可谓词公式与子句集然而，由于谓词公式千变万化，形形色色，给谓词演算的研究带来一定的困难为此，这里先介绍两种谓词演算公式的标准型，也就是范式；因而对谓词演算的研究就可以归结为对范式的研究范式1. 前束形范式一个谓词公式，如果它的所有量词均非否定地出现在公式的最前面，且它的辖域一直延伸到公式之末，同时公式中不出现连接词→及↔，这种形式的公式称作前束形范式例如公式即是一个前束形的范式优点：量词全部集中在公式的前面，此部分称作公式的首标，而公式的其余部分实际上是一个命题演算公式缺点：杂乱无章，量词的排列没有一定的规则范式2. 斯克林范式（Skolem）斯克林范式对前束形范式进行了改进，使得首标中所出现的量词具有一定的规则，即每个存在量词均在全称量词的前面。

如 这是离散数学中有关Skolem范式的定义在人工智能的归结推理研究中，Skolem标准形的定义是，从前束形范式中消去全部存在量词所得到的公式称为Skolem标准形，它的一般形式是其中 是一个合取范式，称为Skolem标准形的母式将谓词公式G化为Skolem标准型的步骤如下1消去谓词公式G中蕴涵符（）和双条件符号（↔ ），以~A B代替A B，以（A B）  （~A  ~B）替换A↔ B2 减少否定符（~）的辖域，使否定符号最多只作用到一个谓词上3 重新命名变元，使所有的变元名字均不同，并且自由变元与约束变元亦不同4 消去存在量词这里分两种情况，一种情况是存在量词不在全称量词的辖域内，此时，只要用一个新的个体常量替换该存在量词约束的变元；另一种情况是，存在量词位于一个或多个全称量词的辖域内，例如：将谓词公式G化为Skolem标准型的步骤（续）此时，变元y实际受前面的变元的约束，需要用Skolem函数 替换y即可将存在量词y消去，得到：5 把全称量词移到公式的左边，并使每个量词的辖域包括这个量词后面公式的整个部分。

6 母式化为合取范式：任何母式都可以写成由一些谓词公式和谓词公式否定的析取的有限集组成的合取将谓词公式G化为Skolem标准型例：将以下谓词公式化为Skolem标准型解 按照将谓词公式化为Skolem标准型的步骤解题如下：（1）取消“→”和“↔”连接词2）把“~”的辖域减少到最多只作用于一个谓词将谓词公式G化为Skolem标准型（续）（3）变量更名4）消存在量词因为存在量词和都在辖域内，属于上述所讲的第二种情况，所以分别用Skolem函数f(x)和g(x)替换y和z5）全称量词移到左边，由于只有一个全称量词，已在左边，所以不移6）将母式化为合取范式子句与子句集n文字：不含有任何连接词的谓词公式叫原子公式，简称原子，而原子或原子的否定统称文字n子句：就是由一些文字组成的析取式如：P(x) ~Q(x,y), ~P(x,c) R(x,y,f(x))都是子句n空子句：不包含任何文字的子句称为空子句，记为NIL由于空子句不包含任何有任何文字，它不能被任何解释满足，所以空子句是永假的，是不可满足的n子句集：由子句构成的集合称为子句集n无量词约束n元素只是文字的析取n否定符只作用于单个文字n元素间默认为和取n例：{~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(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化）原则：对于一个受存在量词约束的变量，如果他不受全程量词约束，则该变量用一个常量代替，如果他受全程量词约束，则该变量用一个函数代替。

(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, 化为合取范式即(ab)  (cd)  (ef)的形式 (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(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标准型的过程中，当消除全称量词左侧的存在量词时，从个体域D中选定的某一个个体a而存在量词具有“或”的含义，只要个体域D中一个个体使G为真，侧G取值就为TSkolem标准型只是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的子句集消解（归结）原理子句集中各子句间的关系是合取的关系，因此，只要有一个子句是不可满足的，则子句集是不可满足的另外，我们在前面已经指出，空子句是不可满足的，所以只要子句集中包含一个空子句，则此子句集就一定是不可满足的。

Robinson的归结原理正是基于这一认识提出来的，其基本思想是：检查子句集S中是否有空子句，若有，则表明S是不可满足的；若没有，就在子句集中选择合适的子句对其进行归结推理，如果能推出空子句，则说明子句集S是不可满足的命题逻辑中的归结原理n互补文字：若P是原子谓词公式或原子命题，则称P与~P是互补文字n归结与归结式：设C1与C2式子句中的任意两个子句，如果C1中的文字L1与C2中的文字L2互补，则从C1与C2中可以分别消去L1和L2，并将二子句中余下的部分做析取构成一个新的子句C12 ，称这一过程为归结，所得到的子句C12称为C1和C2的归结式，而C1和C2称为C12的亲本子句归结推理规则设有两个子句：C1=P∨C1’ 和C2=~P∨C2’ P和~P是两个互补文字，则消去互补文字后得： C12=C1’ ∨C2’ 这一归结过程就是一种推理规则实际上，归结推理方法就只有这么一条规则为了说明推理规则的正确性，应该证明归结式C12是C1和C2的逻辑结论，即要证明： C1∧C2 => C12归结原理要证明： 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’也必为真于是我们得到如下定理：归结原理定理：归结式C12是其亲本子句C1和C2的逻辑结论由它可以得出如下的推论：推论：设C1和C2是子句集S上的子句，C12是C1和C2归结式如果把C12加入子句集S后得到新子句集S1，则S1和S在不可满足的意义下是等价的即：S是不可满足的 S1是不可满足的归结推理过程由上面的推论以及空子句的不可满足性，可以得到证明子句集S不可满足性的推理过程如下：（1）对子句集S中的各子句间使用归结推理规则2）将归结所得的归结式放入子句集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的不可满足性。

n在命题逻辑中，对不可满足的子句集S，归结原理是完备的也就是说，如果子句集S是不可满足的，则必然存在一个从S到空子句的使用归结推理规则的归结推理过程；反之，若存在一个从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 σ})称作子句C1和C2的一个二元归结式，而L1和L2是被归结的文字。

这里使用了集合的符号和运算是为了说明的方便要将子句Ci σ 和Li σ先写成集合形式，如P(x) ∨～ Q(y)改写为{P(x) ，～ Q(y)}在集合的表示下做减法或并运算，然后再写成子句形归结时注意的问题在谓词逻辑中，对子句进行归结推理时，要注意以下几个问题：（1）若被归结的子句中具有相同的变元时，需要将其中一个子句的变元更名例如， C1 =P(x)， C2 =~P(f(x))，尽管由C1和C2组成的子句集S={C1，C2}是不可满足的，但由于C1和C2有相同的变元，无法对其进行合一，从而将无法将它们归结2）在求归结式时，不能同时消去两个互补文字对，消去两个互补文字对所得的结果不是两个亲本子句的逻辑结论如有两个子句C1=P ∨ Q 和C2=~P ∨~ Q若同时消去两个互补文字对（P和~P，Q和~Q），便得到空子句NIL，从而得出C1和C2矛盾的结论，但C1和C2并无矛盾3）如果在参加归结的子句内含有可合一的文字，则在进行归结之前，应对这些文字进行合一，以实现这些子句内部的化简例如，设有如下两个子句：C1=P(x) ∨P(f(a)) ∨ Q(x)C2=~P(y) ∨R(b)由于在子句C1中有可合一的文字P(x)和P(f(a))，若用它们最一般合一θ={f(a)/x}进行置换，得到C1 θ =P(f(a)) ∨ Q(f(a))此时，再对C1 θ和C2进行归结。

选用mgu为σ ={f(a)/y}，得到C1 θ和C2的二元归结式为C12=R(b) ∨Q(f(a))我们把 C1 θ称作C1的因子一般情况下，如果一个子句C的几个文字具有最一般的合一置换σ ，则称C σ为子句C的因子如果C σ是一个单文字，则称它为C的单元因子二元归结式定义 设C1和C2是两个没有相同变元的子句， 则下列四种二元归结式叫做C1和C2的归结式，仍记作C12 1）C1与C2的二元归结式2） C1的因子C1 σ1与C2的二元归结式3） C1与C2的因子C2 σ2的二元归结式4） C1的因子C1 σ1与C2的因子C2 σ2的二元归结式例设C1=~P(a) ∨ Q(x) ∨ R(x)，C2=P(y) ∨ ~Q(b)，求其二元归结式解 若选L1=~P(a)，L2=P(y)，则L1和L2的mgu是σ={a/y}，于是得C1与C2的二元归结式为C12 =( C1 σ –{ L1 σ}) ∪( C1 σ –{ L1 σ}) =({~P(a), Q(x), R(x)}-{~P(a)} )∪({P(a),~Q(b)}-{P(a)}) = ({Q(x), R(x)} )∪({~Q(b)}) =Q(x) ∨ R(x )∨ ~Q(b)若选L1=Q(x)，L2=~Q(b)，则L1和L2的mgu是σ={b/x}，C12 =~P(a) ∨ R(b )∨ P(y)例设C1=P(x) ∨~ Q(x)，C2=Q(f(x))，求其二元归结式。

先将C1的变元更名为y，便可对C1=P(y) ∨~ Q(y)，C2=Q(f(x))进行归结二者的mgu为σ={f(x)/y}，归结式如下C12=P(f(x))例设C1=~Q(f(g(a)))∨ R(b) ，C2= Q(x) ∨ Q(f(y)) ∨ R(g(y))，求其二元归结式解 由于C2中的文字Q(x) 和 Q(f(y)) 存在mgu， σ={f(y)/x}，所以得C2的因子 C2 σ = Q(f(y)) ∨ R(g(y))，将C2 σ与C1进行归结，它们的mgu为 θ={g(a)/y}，得C1和C2的归结式为C12 = R(g(g(a))) ∨ R(b) 对于谓词逻辑，前面的定理仍然有用，即归结式是它的亲本子句的逻辑结论将两个子句的归结式加入子句集S中，所得到的新子句集S’与原子句集S在不可满足的意义下是等价的也就是说，在命题逻辑推理中给出的归结推理过程，在一阶谓词逻辑的推理过程中仍然适用归结原理的完备性我们已使用归结原理建立了证明子句集S不可满足性的推理过程，那么，若一个子句集是不可满足的，是否使用归结推理方法必能得到证明呢？结论是，对于一阶谓词逻辑，从不可满足的意义上说，归结原理是完备的。

即若子句集是不可满足的，则必存在一个从该子句集到空子句的归结推理过程；反之，若从子句集到空子句存在一个归结推理过程，则该子句集必是不可满足的利用归结原理进行定理证明归结原理指明了证明子句集不可满足性的方法对于定理证明，我们经常见到的形式是：A1∧ A2∧ …∧ An →B这里A1∧ A2∧ …∧ An 是前提条件，而B则是逻辑结论根据定理3-1，为了证明B是A1∧ A2∧ …∧ An的逻辑结论，只需证明A1∧ A2∧ …∧ An ∧~B是不可满足的又根据定理3-2，要证明公式的不可满足性，只要证明其相应子句集的不可满足性应用归结原理进行定理证明的步骤如下：设要被证明的定理可用谓词公式表示为如下的形式：A1∧ A2∧ …∧ An →B（1）首先否定结论B，并将否定的公式~B与前提公式集组成如下形式的谓词公式：G= A1∧ A2∧ …∧ An ∧~B（2）求谓词公式G的子句集S3）应用归结原理，证明子句集S的不可满足性，从而证明谓词公式G的不可满足性这就是说对结论B的否定是错误的，推断出定理的成立例已知：A：B：求证：B是A的逻辑结论证明：首先将A和~B化为子句集：(1)~P(x,y) ∨~Q(y) ∨R(f(x))(2)~P(x,y) ∨~Q(y) ∨T(x,f(x))(3)~R(z)(4)P(a,b)(5)Q(b)下面进行归结：(6)~P(x,y) ∨~Q(y) (1)与(3)归结， σ ={f(x)/z}(7)~Q(b) (4)与(6)归结， σ ={a/x,b/y}(8)NIL(空子句） (5)与(7)归结所以B是A的逻辑结论例任何通过了历史考试并中了彩票的人是快乐的。

任何肯学习或幸运的人可以通过所有考试，John不学习但很幸运，任何人只要是幸运的就能中彩求证：John是快乐的证明：第一步，定义谓词将待证明的问题的前提条件和逻辑结论用谓词公式表示出来1）定义谓词：pass(x,y)表示x能通过y考试；win(x,y)表示x能赢得y；Study(x)表示x肯学习；luck(x)表示x很幸运；happy(x)表示x是快乐的（2）将前提及要求证的问题表示成谓词公式：F1：任何通过历史考试并中了彩票的人是快乐的 x)(pass(x,history)∧win(x,lottery)→happy(x))F2：任何肯学习或幸运的人可以通过所有考试 x)( y)(study(x) ∨luck(x)→pass(x,y))F3： John不学习但很幸运~study(John) ∧lucky(John)F4：任何人只要是幸运的就能中彩 x)(luck(x)→ win(x,lottery))G:John是快乐的happy(John)第二步：将上述谓词和~G化成子句集1)~pass(x,history) ∨ ~win(x,lottery) ∨ happy(x)(2) ~study(x)∨ pass(x,y)(3)~ luck(x) ∨pass(x,y)(4) ~study(John) (5) lucky(John)(6) ~luck(x) ∨ win(x,lottery)(7)~ happy(John)第三步：利用归结原理对上面的子句集中的子句进行归结。

8) ~pass(x,history) ∨ happy(x) ∨ ~luck(x) (1)与(6)归结(9) ~pass(John,history) ∨ ~luck(John) (7)与(8)归结σ ={John/x}(10) ~pass(John,history) (5)与(9)归结(11) ~luck(John) (3)与(10)归结σ ={John/x,history/y}(12)NIL (5)与(11)归结这样就由于否定结论“John是快乐的而推出了矛盾，从而证明原来的结论是正确的，即”John是快乐的“ 应用归结原理进行问题求解归结原理不但可以应用于定理证明，而且可以用它来求解问题的答案，其思想与定理证明类似下面是利用归结原理求取问题答案的步骤：（1）把已知前提条件用谓词公式表示出来，并化成相应的子句集，设该子句集的名字为S12）把待求解的问题也用谓词公式表示出来，然后将其否定，并与一谓词ANSWER构成析取式谓词ANSWER是一个专为求解问题而设置的谓词，其变量必须与问题公式的变量完全一致（3）把问题公式与谓词ANSWER构成的析取式化为子句集，并把该子句集与S1合并构成子句集S。

4）对子句集S应用谓词归结原理进行归结，在归结过程中，通过合一置换，改变ANSWER中的变元5）如果得到归结式ANSWER，则问题的答案即在ANSWER谓词中例任何兄弟都有同一个父亲，John和Peter是兄弟，且John的父亲是David，问Peter的父亲是谁？解 第一步：将已知条件用谓词公式表示出来，并化成子句集，那么要先定义谓词1）定义谓词公式设Father(x,y)表示x是y的父亲Brtoher(x,y)表示x和y是兄弟（2）将已知事实用谓词公式表示出来F1：任何兄弟都有同一个父亲 x)( y)( z)(Brother(x,y) ∧Father(z,x) →Father(z,y)F2： John和Peter是兄弟Brother(John,Peter)F3：John的父亲是DavidFather(David,John)（3）将它们化成子句集得S1={~Brother(x,y) ∨ ~Father(z,x) ∨ Father(z,y), Brother(John,Peter), Father(David,John)}第二步：把问题用谓词公式表示出来，并将其否定与谓词ANSWER作析取。

设Peter的父亲是u，则有：Father(u,Peter)将其否定与ANSWER作析取，得G：~Father(u,Peter) ∨ANSWER(u)第三步：将上述公式G化为子句集S2 ，并将S1和S2合并到SS1={~ Father(u,Peter) ∨ANSWER(u)}S= S1∪S2将S中各子句列出如下：（1）~Brother(x,y) ∨ ~Father(z,x) ∨ Father(z,y)（2） Brother(John,Peter)（3） Father(David,John)（4） ~Father(u,Peter) ∨ANSWER(u)第四步：应用归结原理进行归结(5) ~Brother(x,y) ∨ Father(David,John) （1）与（3）归结σ ={David/z,John/x}(6) ~Brother(John,Peter) ∨ANSWER(David) (4)与(5)归结σ ={David/u, Peter/y}(7) ANSWER(David) (2)与(6)归结第五步：得到了归结式ANSWER(David) ，答案即在其中，所以u=David。

即Peter的父亲是David归结方法小结n求子句集，进行归结，方法简单n通过修改证明树的方法，提取回答n方法通用n求解效率低，不宜引入启发信息n不宜理解推理过程习题1假设有以下前提知识：（1）自然数是大于零的整数2）所有整数不是偶数就是奇数3）偶数除以2是整数求证：所有自然数不是奇数就是其一半为整数的数2 某人被盗，公安派出所排出5个侦察员去调查研究案情时，侦察员A说：“赵与钱中至少一人作案”；侦察员B说：“钱与孙中至少一人作案”；侦察员C说：“孙与李中至少一人作案”；侦察员D说：“赵与孙中至少有一人与此案无关”；侦察员E说：“钱与李中至少有一人与此案无关”如果这5个侦察员的话都是可信的，试问谁是盗窃犯呢？人有了知识，就会具备各种分析能力，明辨是非的能力所以我们要勤恳读书，广泛阅读，古人说“书中自有黄金屋通过阅读科技书籍，我们能丰富知识，培养逻辑思维能力；通过阅读文学作品，我们能提高文学鉴赏水平，培养文学情趣；通过阅读报刊，我们能增长见识，扩大自己的知识面有许多书籍还能培养我们的道德情操，给我们巨大的精神力量，鼓舞我们前进。