哈工大人工智能课件chpt4

人工智能原理

第4章消解法

1人工智能原理

第4章消解法1

本章内容

4.1消解法的基本思想

4.2消解法

4.3消解策略

4.4Herbrand定理

参考书目第4章消解法2 本章内容

4.1消解法的基本思想

4.24.1消解法的基本思想第4章消解法34.1消解法的基本思想第4章消解法3消解法的基本思想从第3章逻辑系统中可知，逻辑推理必须考虑其有效性(即∑|=A)，即对论域中的任何赋值都能保证公式为真从有效性和可满足性的关系可知，有效性等价于其否命题的不可满足性证明一个逻辑公式的有效性就是证明其公式的非的不可满足性(恒为假)这样就引出了消解法，其基本思想就是反证法第4章消解法4消解法的基本思想从第3章逻辑系统中可知，逻辑推理必须考虑其有消解法基本思想:反证法即：要证命题(理解为经典逻辑的公式)A恒为真，等价于证﹁A恒为假从语义上解释，恒为假就是不存在一个论域上的一个赋值(可称为解释)，使﹁A为真，即对所有的论域上的所有赋值，﹁A均为假但是，论域本身和解释有无穷多个，不可能一一验证第4章消解法5消解法基本思想:反证法即：要证命题(理解为经典逻辑的公式)A基本思想(1)Herbrand提出：从所有解释当中选出一种有代表性的解释，并严格证明一旦命题在代表性解释中为假，则在所有解释中为假Herbrand定义了这样的论域和代表性解释，称为Herbrand论域(H论域)和Herbrand解释(H解释)后面会看到：公式A(无前束范式)是不可满足的，当且仅当A(通过子句集)在所有Herbrand赋值下都取假值第4章消解法6基本思想(1)Herbrand提出：从所有解释当中选出一种有基本思想(2)这样，在证假(不可满足)的意义上使公式与子句集的语义解释等价、并与H解释等价，作为消解法的开端引入语义树，让所有解释都展现在语义树上，以便找到H解释。最后在改进寻找解释算法的复杂性中发现了消解式，从而构成了消解法的完整理论基础消解也叫归结，本章混用这两个称呼第4章消解法7基本思想(2)这样，在证假(不可满足)的意义上使公式与子句集4.2消解法

4.2.1公式到子句集的转换

4.2.2合一算法

4.2.3消解式

4.2.4消解法的实施第4章消解法84.2消解法

4.2.1公式到子句集的转换

4.2消解法的形式消解法举例：此时只要使用单文字删除规则就可以推出结论Q。但是如果子句中包含变量，则常常必须经过变量置换才能进行消解第4章消解法9消解法的形式消解法举例：第4章消解法9归结规则归结—两个互补文字消去单元归结规则—一个子句和一个文字进行互补文字消去全归结规则—两个子句中消去互补文字第4章消解法10归结规则归结—两个互补文字消去第4章消解法10公式与子句集的等价有定理S：给定公式A及相应的子句集S，则A是不可满足的当且仅当S是不可满足的实现消解法的基础是把参与推理的每个公式都转化为子句集/通过逐步对消子句集合中互补的文字(即L和﹁L)而最终得到一个空子句□，证明原来的公式是不可满足的第4章消解法11公式与子句集的等价有定理S：给定公式A及相应的子句集S，则A消解法证明的步骤证明一个公式A在给定论域下恒为真，也就是要证明﹁A恒为假将﹁A转化为一个子句集，集合中元素为原子公式或其析取/通过其中正负原子公式的合并(此时恒为真，对证假不起作用，因此消去)/最后集合为空，说明是不可满足的，即恒为假通常形式：证明﹁(A→B)为假即A∧﹁B为假，也即对应子句集归结为空子句第4章消解法12消解法证明的步骤证明一个公式A在给定论域下恒为真，也就是要证消解法证明的步骤写出谓词关系公式用反演法写出谓词表达式SKOLEM标准型子句集S对S中可消解的字句进行消解（先进行合一置换）消解式仍放入S中，反复消解过程得到空字句得证13消解法证明的步骤写出谓词关系公式134.2.1公式到子句集的转换首先复习几个定义：文字(literal)：正原子公式和负原子公式称为文字，同一原子公式的正和负称为互补的子句(clause)：文字的析取称为子句合取范式：形如A1∧A2∧…∧An的公式，其中A1～An均为子句前束范式：形如(Q1x1…Qnxn)M(x1…xn)的公式，M中不再含有量词，Q是量词Skolem标准形：在前束范式中消去存在量词后得到的公式第4章消解法144.2.1公式到子句集的转换首先复习几个定义：第4章消解消去存在量词消去存在量词的步骤：(1)若存在量词不在任何全称量词之后，则公式中被存在量词量化的变量以某个不同于公式中任何其他常量名字的常量c代替，并消去存在量词；(2)若存在量词在k个全称量词之后，则公式中被存在量词量化的变量用被前k个全称量词量化的变量x1～xk的某个函数f(x1～xk)的形式代替，f的名字不同于公式中任何其他函数的名字，但对函数形式没有要求；然后消去存在量词/函数f称为Skolem函数第4章消解法15消去存在量词消去存在量词的步骤：第4章消解法15公式转化为子句集的步骤(1)公式A化为子句集S，其实现步骤共9步，如下：(1)消去等价和蕴含符号：蕴含转化为析取(2)将否定符号转移到每个谓词之前：应用狄摩根定律(3)变量标准化：约束变量各不相同(4)公式化为前束型：全部存在量词和全称量词移到公式的最前面/得到的两部分称为前缀和母式第4章消解法16公式转化为子句集的步骤(1)公式A化为子句集S，其实现步骤共公式转化为子句集的步骤(2)(5)消去存在量词：存在量词不受全称量词约束，则变量用常量替换/如果存在量词受全称量词约束，则使用Skolem函数替换相应变量——得到Skolem标准形(6)母式化为合取范式：外层连接符全部是合取，里层连接符全部为析取(7)去掉所有全称量词(8)母式化为子句集：每个合取项间的合取符号(∧)用逗号代替，即得子句集(9)子句变量标准化：每个子句中的变量各不相同第4章消解法17公式转化为子句集的步骤(2)(5)消去存在量词：存在量词不受4.2.2合一算法[定义]置换(或代换)：设x1～xn是n个变量，且各不相同，t1～tn是n个项(常量、变量、函数)，ti≠xi，则有限序列{t1/x1,t2/x2…tn/xn}称为一个置换置换可以作用于谓词公式，也可以作用于项。置换θ={t1/x1,t2/x2…tn/xn}作用于谓词公式E就是将E中变量xi均以ti代替，其结果用E表示/作用于项的含义相同第4章消解法184.2.2合一算法[定义]置换(或代换)：设x1～xn是n关于置换例：={a/x,f(b)/y,u/z}E=P(x,y,z) t=g(x,y)E=P(a,f(b),u) t=g(a,f(b))[定义]置换乘积(合成)：设和是2个置换，则先后作用于公式或项，称为置换乘积，用表示(E)一般来说，置换乘积的结合律成立，即()=()，但交换律不成立第4章消解法19关于置换例：={a/x,f(b)/y,u/z}第4章合一置换[定义]合一置换：设有一组谓词公式{E1～Ek}和置换，使E1=E2=…=Ek，则称为合一置换，E1～Ek称为可合一的。合一置换也叫通代[定义]最一般合一置换(最广通代)：如果和都是公式组{E1～Ek}的合一置换，且有置换存在，使得=，则称为公式组{E1～Ek}的最一般合一置换，记为mgu(mostgeneralunification)第4章消解法20合一置换[定义]合一置换：设有一组谓词公式{E1～Ek}和置分歧集在介绍mgu求解算法之前，首先说明什么是分歧集

/合一的过程就是消除分歧[定义]分歧集(不一致集)：设W是一个非空谓词集，从左至右逐个比较W中的符号，如果在第i(i1)个符号处W中各谓词第一次出现分歧(即至少存在Ej和Ek在第i个符号处不一样，而在i之前各谓词符号均一样)，则全体谓词的第i个符号构成了W的分歧集D。分歧集性质：分歧集的出现处一定是谓词或项的开始处/求最广合一置换只考察项的分歧第4章消解法21分歧集在介绍mgu求解算法之前，首先说明什么是分歧集/合mgu求解算法求mgu算法(合一算法)设W是谓词组，表示空置换(即置换序列为空)，则算法如下：(1)k=0，W0=W，0=；(2)如果Wk中各谓词完全一样，则算法结束，k是W的mgu，否则求Wk的分歧集Dk；(3)若Dk含变量xk以及项tk的首符号且xk在tk中不出现，则继续执行算法，否则W的mgu不存在，算法停止；(4)令k+1=k{tk/xk}，Wk+1=Wk{tk/xk}；(5)k=k+1，转(2)第6章消解法22mgu求解算法求mgu算法(合一算法)第6章消解法22mgu存在条件mgu存在的条件：如果有限谓词组W是可合一的，则上述算法一定成功结束并给出其存在求mgu的预置条件：应把所有谓词中的变量换成不同名字的变量。(不过，这在将公式化为子句集时已经完成。)第4章消解法23mgu存在条件mgu存在的条件：如果有限谓词组W是可合一的，mgu求解例子(1)例1：求W={P(a,x,f(g(y))),P(z,f(a),f(u))}的mgu(1)0=，W0=W，D0={a,z}(2)1=0{a/z}={a/z}，W1=W01={P(a,x,f(g(y))),P(a,f(a),f(u))}，D1={x,f(a)}(3)2=1{f(a)/x}={a/z,f(a)/x}，W2=W12={P(a,f(a),f(g(y))),P(a,f(a),f(u))}，D2={g(y),u}(4)3=2{g(y)/u}={a/z,f(a)/x,g(y)/u}，W3=W23={P(a,f(a),f(g(y))),P(a,f(a),f(g(y)))},D3=此时W已合一，mgu=3={a/z,f(a)/x,g(y)/u} ★第4章消解法24mgu求解例子(1)例1：求W={P(a,x,f(g(ymgu求解例子(2)例2：求W={P(x,x),P(x,f(x))}的mgu首先换名：W={P(x,x),P(y,f(y))}(1)0=，W0=W，D0={x,y}(2)1={x/y}，W1={P(x,x),P(x,f(x))}，D1={x,f(x)}(3)2不存在，因为f(x)中含有变量x。故W的mgu不存在。★第4章消解法25mgu求解例子(2)例2：求W={P(x,x),P(x,4.2.3消解式[定义]文字合并规则：若子句C含有n(n>1)个相同的文字(也称为句节)，则删去其中的n-1个，结果以[C]表示。[定义]因子：若子句C中的多个文字具有mgu，则[C]称为C的一个因子。当[C]为单文字时称为C的单因子通过取因子可以简化一个子句。这是因为取因子之后，子句C中可能出现相同的文字，而根据文字合并规则就可以删除重复部分第4章消解法264.2.3消解式[定义]文字合并规则：若子句C含有n(n>例子：C=P(x,a)∨P(b,y)∨Q(x,y,c)，={b/x,a/y}则[C]=[P(b,a)∨P(b,a)∨Q(b,a,c)]=P(b,a)∨Q(b,a,c)27例子：27二元消解式[定义]二元消解式：设C1、C2是无公共变量的子句，分别含文字L1、L2，而L1和L2有mgu，则子句R(C1,C2)=[(C1L1)∨(C2L2)] 称为C1和C2的二元消解式，其中(C1L1)和(C2L2)分别表示从C1、C2删去L1、L2所余部分。L1和L2称为被消解的文字，C1、C2称为父子句第4章消解法28二元消解式[定义]二元消解式：设C1、C2是无公共变量的子句二元消解式例子例子： 设C1=P(x)∨Q(x),C2=P(g(y))∨Q(b)∨R(x)，则C1和C2有2个二元消解式(一个消P，一个消Q) 如果取={g(y)/x}，得R(C1,C2)=Q(g(y))∨Q(b)∨R(g(y)) 如果取={b/x}，得R(C1,C2)=P(b)∨P(g(y))∨R(b)★注意：求消解式不能同时消去2个互补对文字，如同时消去P和P、Q和Q，那样所得结果就不是C1,C2的逻辑结果了第4章消解法29二元消解式例子例子：第4章消解法29子句的二元消解式子句的二元消解式：以下4种二元消解式都是子句C1和C2的二元消解式：

(1)C1和C2的二元消解式；

(2)C1的一个因子(即经过取因子处理)和C2的二元消解式；

(3)C1和C2的一个因子的二元消解式；

(4)C1的一个因子和C2的一个因子的二元消解式第4章消解法30子句的二元消解式子句的二元消解式：以下4种二元消解式都是子句4.2.4消解法的实施消解法的实施：为证├A→B，则建立G=A∧﹁B(﹁(A→B))，再求出G对应的子句集S，进而只需证明S是不可满足的为证S的不可满足，只要对S中可以消解的子句求消解式，并将消解式(新子句)加入S中，反复进行这样的消解过程直到产生一个空子句□第4章消解法314.2.4消解法的实施消解法的实施：为证├A→B，则建立G消解的注意事项1.谓词的一致性，P()与Q()，不可以2.常量的一致性，P(a,…)与P(b,…)，不可以；但是P(a,…)与P(x,…)，可以3.变量与函数，P(a,x,…)与P(x,f(x),…)，不可以；但是P(a,x,…)与P(x,f(y)…)，可以4.不能同时消去两个互补对5.先进行内部简化（置换、合并）32消解的注意事项1.谓词的一致性，P()与Q()，不可以消解法举例“快乐学生”问题假设：任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可以通过所有考试，张不肯学习但他是幸运的，任何幸运的人都能获奖。求证：张是快乐的。证明过程：所有假设表示为一个子句集，加入结论的否定以后进行消解第4章消解法33消解法举例“快乐学生”问题第4章消解法33第4章消解法34第4章消解法34第4章消解法35第4章消解法35第4章消解法36第4章消解法364.3消解策略

4.3.1

常用消解策略

4.3.2支持集消解

4.3.3有序消解策略

4.3.4消解法举例第4章消解法374.3消解策略

4.3.1常用消解策略

4.3.2消解过程的计算复杂性定理证明的过程就是在子句集S中不断求消解式，直到生成一个空子句□现在涉及到求消解式的计算复杂性问题，通常不考虑任何消解策略的盲目消解具有指数级的计算量：对于有n个子句的子句集，如果进行i次求消解式后得到空子句，则计算复杂性是O(n2i)所以要研究加快消解速度、提高效率的各种消解策略第4章消解法38消解过程的计算复杂性定理证明的过程就是在子句集S中不断求消解4.3.1常用消解策略相关的消解策略主要包括：删除无用的子句—永真式和隐含子句求隐含关系—归类算法禁止无用子句产生—限制参加消解的子句/限制被消解的文字/限制消解方式第1种策略：支持集策略和动态支持集策略常用动态支持集策略—线性消解/输入消解/单元消解第2种策略—有序消解第4章消解法394.3.1常用消解策略相关的消解策略主要包括：第4章消解删除策略删除策略—最直观的一种策略就是删除对消解没有任何贡献的子句，减少进行消解的子句数量，从而提高效率删除哪些子句？有2类：永真式和隐含式第1类是重言式(永真式)，即包含﹁P∨P形式的子句，因为它是永远被满足的，对判定不可满足性没有作用第4章消解法40删除策略删除策略—最直观的一种策略就是删除对消解没有任何贡献隐含关系另一类是被子句集中其他子句所隐含的子句首先定义隐含关系[定义]设C1、C2是2个子句，lit(Ci)表示Ci中各个文字的集合，如果存在置换，使lit(C1)lit(C2)，则称C1隐含C2(C2被C1隐含)，或称C1把C2归类[定理]如果S中的子句C1隐含C2，则S是不可满足的当且仅当S{C2}是不可满足的第4章消解法41隐含关系另一类是被子句集中其他子句所隐含的子句第4章消解法归类算法(1)为了说明求隐含关系的算法(也称归类算法)，首先说明求隐含关系也化为消解问题给定子句C、D，x1xn是D中所有变量，a1an是C、D中均未出现的常量，令={a1/x1…an/xn}设D=L1∨…∨Lm，令﹁D=﹁L1∧…∧﹁Lm，则求隐含关系就成为C与W={﹁L1,…﹁Lm}消解为空子句的过程第4章消解法42归类算法(1)为了说明求隐含关系的算法(也称归类算法)，首先归类算法(2)归类算法：给定子句C、D，并令W={﹁L1,…﹁Lm}，其中如上述定义

(1)设i=0，U0={C} (2)如果Uk包含□，则C隐含D，算法停止

(3)令Uk+1={R(C1,C2)|C1∈Uk,C2∈W} (4)如果Uk+1=Φ，则C不隐含D，算法停止

(5)i=i+1，转(2)。第4章消解法43归类算法(2)归类算法：第4章消解法43归类算法(3)注意：Uk+1=Φ表明Uk和W中已不存在可消解的子句，所以没有R(C1,C2)，其中C1∈Uk,C2∈W第4章消解法44归类算法(3)注意：Uk+1=Φ表明Uk和W中已不存在可消解归类算法举例

例子：C=﹁P(x)∨Q(f(x),a) D=﹁P(h(y))∨Q(f(h(y)),a)∨P(z)首先作={b/y,c/z}，则W={P(h(b)),﹁Q(f(h(b)),a),﹁P(c)}={W1,W2,W3}(1)U0={C}={﹁P(x)∨Q(f(x),a)}(2)U0不包含□，则U1={R(C,W)}={Q(f(h(b)),a),﹁P(h(b))}，其中Q(*)是U0与W1的消解式，﹁P(*)是U0与W2的消解式，U1不空继续(3)U2显然包含□，因为Q(f(h(b)),a)∈U1而﹁Q(f(h(b)),a)∈W可消解为□，同样﹁P(h(b))∈U1而P(h(b))∈W可消解为□。★第4章消解法45归类算法举例例子：C=﹁P(x)∨Q(f(x),a)禁止无用子句产生禁止无用子句的产生：删去重言式和被隐含子句的策略提示我们，如果不让无用子句产生，其效率会更高。因为检查哪些子句是无用的也要花费时间。禁止无用子句的产生可以通过下述三个方面来进行：

(1)限制参加消解的子句；

(2)限制子句中被消解的文字；

(3)限制消解的方式。主要介绍第1种策略，即对每次参加消解的子句作出规定第4章消解法46禁止无用子句产生禁止无用子句的产生：删去重言式和被隐含子句的支持集消解[定义]支持集消解：设S为子句集，S’为其子集，若S―S’是可满足的，则称S’是S的一个支持集。如果限定消解双方不能都取自S―S’，则此消解称为支持集消解给定S’之后，若每一步消解都是支持集消解，则此推导称为支持集推导，其结果为空子句时称为支持集否证。注意：这里只要说明S―S’可满足即可，并未指明S’不可满足，但此时必然指定某种真值规定第4章消解法47支持集消解[定义]支持集消解：设S为子句集，S’为其子集，若4.3.2支持集消解一般来说，消解法常常用来证明C1∧C2∧…∧Cn∧﹁C不可满足，此即C1∧C2∧…∧Cn→C因为前提子句集合{Ci}应该是可满足的，所以消解不应在各个Ci间进行，而应在Ci和﹁C之间或﹁C内部进行支持集策略：推广此想法，限定消解双方不能都取自子句集的某个子集第4章消解法484.3.2支持集消解一般来说，消解法常常用来证明C1∧C2支持集消解例子[定理]支持集消解是完备的，即S是不可满足的当且仅当存在一个以S’为支持集的否证，其中S’是S的子集，S―S’是可满足的。例1：S={P∨Q,﹁P∨Q,P∨﹁Q,﹁P∨﹁Q}，则S’={﹁P∨﹁Q}是S的支持集(当P、Q取真值时S―S’可满足)。其消解过程可由下图说明第4章消解法49支持集消解例子[定理]支持集消解是完备的，即S是不可满足的当动态支持集消解判断S―S’是否可满足，需要花费时间，所以要寻找更好的策略。支持集消解的进一步改进就得到了动态支持集消解[定义]动态支持集消解：设S是子句集，S0=S，Sn=Sn-1∪{Cn}，其中Cn是Sn中两个子句的消解式，如果有一种根据子句的语法结构划分子句集的统一方法，使每个Sn都划分为Sn1和Sn2两部分，且在消解时限定双方不能都取自Sn1

，则称Sn2是Sn的一个动态支持集，此消解称为动态支持集消解。同时亦定义动态支持集推导、动态支持集否证。第4章消解法50动态支持集消解判断S―S’是否可满足，需要花费时间，所以要寻常用动态支持集消解策略常用的动态支持集消解有下列几种策略：

(1)线性消解

(2)输入消解

(3)单元消解[线性消解定义]在动态支持集消解定义中令Sn2={Cn}，则此策略称为线性消解策略。Cn称为消解时的中心子句，另一方称为边子句线性消解是完备的第4章消解法51常用动态支持集消解策略常用的动态支持集消解有下列几种策略：第线性消解注意：在现行消解过程中，初始中心句的选取很重要，不能任意选择。例2：S={P∨Q,﹁P∨Q,P∨﹁Q,﹁P∨﹁Q}，其线性消解过程可由下图说明。★第4章消解法52线性消解注意：在现行消解过程中，初始中心句的选取很重要，不能输入消解[输入消解定义]在动态支持集消解定义中令Sn2=S，则此策略称为输入消解策略。因为每次消解必须有原子句集S中的子句参加(即输入子句)由此得名例3：S={﹁P,P∨﹁Q,Q∨﹁R,R}，其消解过程如图所示。★第4章消解法53输入消解[输入消解定义]在动态支持集消解定义中令Sn2=S，单元消解[单元消解定义]在动态支持集消解定义中令Sn2={Sn

中所有单子句和单因子}，则此策略称为单元消解策略(也叫单项消解)/这样，每次参加消解的一方总有一个是单项例4：S={P∨Q,﹁P∨R,﹁Q∨R,﹁R}，其消解过程如图所示。★第4章消解法54单元消解[单元消解定义]在动态支持集消解定义中令Sn2={S4.4Herbrand定理

4.4.1公式到子句集的转换

4.4.2Herbrand论域和解释

4.4.3语义树

4.4.4Herbrand定理

4.4.5不可满足基子句集第4章消解法554.4Herbrand定理

4.4.1公式到子句集的4.4.2Herbrand论域和解释Herbrand论域定义Herbrand论域(H论域)：设S为子句集，H0是S中子句所含的全体常量集，若S中子句不含常量，则任选一常量a令H0={a}。 对i≥1令Hi=Hi-1∪{f(t1,…tn)|n≥1 f是S中的任一函数符号，t1,…tn是Hi-1中的元素 则Hi称为S的i阶常量集，H∞称为S的Herbrand论域，其元素称为基项。第4章消解法564.4.2Herbrand论域和解释Herbrand论域定H论域例子例1：S={P(a),﹁P(a)∨P(f(x))}根据定义有H0={a}/H1={a}∪{f(a)}={a,f(a)}H2={a,f(a)}∪{f(a),f(f(a))}={a,f(a),f(f(a))} ……H∞={a,f(a),f(f(a))…} ★例2：S={P(x),Q(f(a))∨﹁R(g(b))}H0={a,b}/H1={a,b,f(a),f(b),g(a),g(b)}H2={a,b,f(a),f(b),g(a),g(b),f(f(a)),f(f(b)),f(g(a)),…} ……H∞={a,b}∪{f(c),g(d)|c,dH∞} ★第4章消解法57H论域例子例1：S={P(a),﹁P(a)∨P(f(x))Herbrand原子集Herbrand原子集定义Herbrand基(原子集)：设S为子句集，H∞是其H论域，则

称为S的H基，~H中元素称为基原子/此为S中所有原子公式取H论域上所有可能值的集合对于例1，其~H={P(a),P(f(a)),P(f(f(a))),…} 对于例2，其~H={P(a),Q(a),R(a),P(b),Q(b),R(b),P(f(a)),Q(f(a)),R(f(a)),P(f(b))…} ★第4章消解法58Herbrand原子集Herbrand原子集定义第4章消解Herbrand解释(1)Herbrand解释是一种语义结构，子句集S的H解释由下列基本部分组成：(1)基本区域H∞(H论域对应U)(2)S的每个常量c对应H域中的同一c(3)S的每个变量在H域中取值(4)S中每个函数fn对应于一个映射H∞×H∞×…×H∞(n个)→H∞，使得对于(t1,t2,…tn)H∞则f(t1,t2,…tn)H∞(5)S中的每个谓词Pn对应于一个映射H∞×H∞×…×H∞(n个)→{T,F}第4章消解法59Herbrand解释(1)Herbrand解释是一种语义结构Herbrand解释(2)该定义表明，一旦给定一个子句集，其H解释基本就确定了/唯一留下的自由度是由谓词P代表的映射即~H到{T,F}的映射。~H可以分解如下：~H=~H1∪~H2h~H1，v(h)=T；h~H2，v(h)=F这样，一旦给出~H1或~H2，则H解释就完全确定了，通常是给出~H1第4章消解法60Herbrand解释(2)该定义表明，一旦给定一个子句集，其H解释例子例子：在例2中设含有常量a的谓词都为T，含有常量b的谓词都为F，则S的H解释={P(a),Q(a),R(a),P(f(a)),Q(f(a)),R(f(a)),P(f(f(a))…}★有定理：若子句集S对所有H解释是不可满足的，则对S的任意解释也是不可满足的第4章消解法61H解释例子例子：第4章消解法614.4.3语义树语义树的表示：要寻找S的H解释的不可满足性质，可以把所有H解释展现在一棵语义树上，然后观察S对应的各个原子公式的真假值。这是一种很直观的研究方式，称为语义树方法设S={P,Q,R}，则H∞={a}，~H={P(a),Q(a),R(a)}(只有一个常量a，在语义树中可省略)因为是二值逻辑，研究每个基原子(即S的原子公式)的取值可以通过原子及其否定(即文字)来观察/构造如下二叉形式的语义树第4章消解法624.4.3语义树语义树的表示：要寻找S的H解释的不可满足性语义树示例通常用I(Ni)表示从根节点到节点Ni分枝上所标记的所有文字的并集。如： I(N22)={P,Q}，I(N35)={P,Q,R}第4章消解法63语义树示例通常用I(Ni)表示从根节点到节点Ni分枝上所标记语义树定义(1)子句集S语义树的定义[定义]设子句集S，对应H基为~H，S的语义树ST定义如下：(1)ST是一棵树；(2)ST的节点均不带标记，而边的标记是基原子且不包含其中的变量(边的标记可能不止一个，用逗号分割)；(3)从每个非叶节点只生成有限个边L1Ln，令Qi是每个Li的标记的合取，则Q1Q2…Qn为永真；(4)从根节点到任一叶子节点的路径上，所有边的标记的并集中不含重复的基原子，也不含互补的基原子第4章消解法64语义树定义(1)子句集S语义树的定义第4章消解法64语义树定义(2)[定义]规范语义树：如果一棵语义树的每条边的标记均为一个原子公式[定义]完备语义树：如果一棵语义树从根节点到任一叶节点的路径上所有边标记的并集中包含子句集中每个原子或其负原子，则该语义树称为完备的(完全的)第4章消解法65语义树定义(2)[定义]规范语义树：如果一棵语义树的每条边的语义树定义(3)对于给定的S，其语义树一般都不唯一。下图中语义树和前图中的语义树对应于同一个H基。这两个图的语义树都是完备的第4章消解法66语义树定义(3)对于给定的S，其语义树一般都不唯一。下图中语语义树和H解释因为一般H基是个无穷集合，所以其对应的语义树也是无限的因为在完备语义树的每一条路径上都有S的全部原子(或负原子)，所以对这些原子公式的真值判定就能决定S的一个解释对于有限完备语义树来说，如果N是一个叶节点，则I(N)便是S的一个H解释/这样，S的不可满足性就与完备语义树路径的真值计算联系起来第4章消解法67语义树和H解释因为一般H基是个无穷集合，所以其对应的语义树也封闭语义树[定义]基例：如果S的某个子句C中所有变量符号均以S的H域的元素(常量)代入时，所得的子句C’称为C的一个基例[定义]否节点：如果语义树节点N的从根节点到N的路径I(N)使S的某个子句的某个基例为假，而其父辈节点不能判断此事实(即I(N)是使基例为假的最小路径)，则称N为否节点(或失败节点)[定义]封闭语义树：如果一棵完全语义树的每个分枝上都有一个否节点，则称为封闭语义树第4章消解法68封闭语义树[定义]基例：如果S的某个子句C中所有变量符号均以封闭语义树例子(1)例：设子句集S={﹁P(x)∨Q(x),P(f(x)),﹁Q(f(x))}

包括3个子句:﹁P(x)∨Q(x),P(f(x), ﹁Q(f(x))

则H∞={a,f(a),f(f(a)),…} H基={P(a),Q(a),P(f(a)),Q(f(a)),…}其封闭语义树如下图所示第4章消解法69封闭语义树例子(1)例：设子句集S={﹁P(x)∨Q(x),封闭语义树例子(2)第4章消解法70封闭语义树例子(2)第4章消解法70封闭语义树例子(3)封闭语义树中每个否节点用★表示在上图中，每个否节点的路径为：I(N2/2)={P(a),﹁Q(a)}，使(﹁P(a)∨Q(a))=F；I(N3/2)={P(a),Q(a),﹁P(f(a))}，使P(f(a))=F；I(N4/9)={﹁P(a),Q(a),P(f(a)),Q(f(a))}，使Q(f(a))=F如此等等上述每个路径所代表的解释已经使S的某个子句为假，因此再扩充路径仍然只能使同一子句为假，所以没有扩充、延伸的必要 □第4章消解法71封闭语义树例子(3)封闭语义树中每个否节点用★表示第4章消有限封闭语义树上例说明，从不可满足的角度来说，对于无限完备语义树只需搜索到一个否节点，则该分枝即被证明为不可满足。这样实际上构成的是一个有限树所以就有Herbrand定理：子句集S不可满足，当且仅当它所对应的每棵完备语义树均包含一个有限的封闭子树(封闭语义树)第4章消解法72有限封闭语义树上例说明，从不可满足的角度来说，对于无限完备语作业1.将合式公式化为子句型2.求出下列子句集的最一般合一（mgu）3“有些患者喜欢任一医生，没有任一患者喜欢任一庸医，所以没有庸医”用消解法证明上述结论73作业1.将合式公式化为子句型73参考书目StuartRussell/PeterNorvig:AIMA第7章/第9章陆汝钤编著:人工智能(下册)第17章石纯一、黄昌宁、王家[广钦]，人工智能原理，清华大学出版社，1993年10月第1版田盛丰、黄厚宽，人工智能与知识工程，中国铁道出版社，1999年8月第1版,第5章第4章消解法74参考书目StuartRussell/PeterNor附录75附录75子句的推导子句的推导定义：给定子句集S，如果存在一个有限的子句序列C1,C2,…,Ck，使得每个Ci或者属于S，或者是C1∼Ci-1的某些子句的消解式，且Ck=C，则从S可以推导出子句C，称此子句序列为C的推导。当C为空子句□时，也称该序列为S的一个否证。第4章消解法76子句的推导子句的推导定义：第4章消解法76Herbrand定理证明Herbrand定理有两种形式Herbrand定理I：子句集S不可满足，当且仅当它所对应的每棵完备语义树均包含一个有限的封闭子树(封闭语义树)证明：[充分性]设S是不可满足的，T是S的一株完备语义树。设B是T的任意一个分支路径，则IB是对应该分支上S的一个解释 由S的不可满足性知IB使S的某子句的某个基例为假。则B上有节点N且N是T的否节点第4章消解法77Herbrand定理证明Herbrand定理有两种形式第4章Herbrand定理I的证明 因为S中子句的个数有限，每个子句所含的文字也有限，则IB中的文字个数也有限，因此否节点N离T的根节点只有有限步。 因为T是二叉树且每个节点只有两个子节点，由B的任意性可知，T所有分支上的否节点所构成的封闭语义树必是有限的。[必要性]已知S存在有限的封闭语义树T。设I是S的任一解释，则其落在T的某个分支B上，B上必有否节点N存在 可知I(N)使S的某子句的某个基例C’为假。由I(N)I及任意性，可知S是不可满足的 ★第4章消解法78Herbrand定理I的证明 因为S中子句的个数有限，每个子Herbrand定理II(1)Herbrand定理II：S是不可满足的，当且仅当存在S的一个不可满足的有限基例集证明：[充分性]设S是不可满足的，及T是S的一个完备语义树。由Herbrand定理I知存在T的有限封闭子树T’。T’存在有限路径和末端否节点，即使S的某个子句的某基例为假。

将基例加起来，即得一个不可满足的有限基例集第4章消解法79Herbrand定理II(1)Herbrand定理II：S是Herbrand定理II(2)[必要性]设S’S且不可满足的有限基例集。设I是S的任一解释，应有S’的解释I’I，已知I’使S’的某个基例为假，于是I使其为假，即使S为假，故S不可满足

★如同语义树的结构不唯一，不可满足的有限基子句集也不唯一从自动证明的角度，定理II是基础第6章消解法80Herbrand定理II(2)[必要性]设S’S且不可满足不可满足基子句集不可满足基子句集的生成：可通过逐步测试基子句集中各有限子集的方法来找出，此为Gilmore算法(算法略，参见陆著)/当S不可满足时，该算法一定结束(半可判定)但该算法具有指数复杂性，为此提出了改进规则，改进的规则称为Davis-Putnam预处理第4章消解法81不可满足基子句集不可满足基子句集的生成：可通过逐步测试基子句Davis-Putnam预处理(1)Davis-Putnam预处理：(1)重言式(永真式)删除规则：删去所有重言式子句，因为与不可满足性无关；(2)单文字(单句节)删除规则：如果S中包含一个单文字子句L(即只有一个原子公式)，则从S中删去所有含L的子句，从S中删去所有子句中的﹁L文字。经过如此处理的子句集为S’，若S’为空，则S是可满足的，若S’非空，则S’与S同是不可满足的；(3)纯文字删除规则：如果S中只包含文字L而不包含﹁L，则删去所有包含L的子句；第4章消解法82Davis-Putnam预处理(1)Davis-PutnamDavis-Putnam预处理(2)(4)分离规则(分裂规则)：如果

S=(L∨A1)∧…∧(L∨Am)∧(﹁L∨B1)∧…∧(﹁L∨Bn)∧R 其中Ai、Bj、R皆不包含L或﹁L，则令

S1=A1∧…∧Am∧RS2=B1∧…∧Bn∧R S是不可满足的等价于S1∨S2是不可满足的(即S1、S2同时不可满足)。经过Davis-Putnam预处理以后的子句集与原子句集在不可满足性上等价第4章消解法83Davis-Putnam预处理(2)(4)分离规则(分裂规则消解法的合理性[合理性定理]若从子句集S可以推导出子句C，则C是S的逻辑推论(或S逻辑蕴含C)。[推论]若S是可满足的，则S推导出的任一子句也是可满足的，即不能推出空子句。其逆否形式：若S推导出空子句□，则S是不可满足的。此为消解原理的合理性定理。即只要找出一个推出空子句的过程，则S就不可满足第4章消解法84消解法的合理性[合理性定理]若从子句集S可以推导出子句C，则消解法的完备性(1)消解法是完备的—即如果公式X是子句集S的逻辑推论，则X可以从S中推出[完备性定理]子句集S是不可满足的，当且仅当从S可推导出空子句□消解过程与语义树倒塌之间的联系：从S的语义树T出发，必有两个否节点所对应的子句可作归结，将归结式放入S，则否节点的位置提升，即原来两个否节点的父节点成为否节点。从而使新否节点下面的语义树分支无必要存在，即引起语义树的倒塌第4章消解法85消解法的完备性(1)消解法是完备的—即如果公式X是子句集S的消解法的完备性(2)重复上述语义树的倒塌过程，直到语义树仅由树根组成为止。此时树根是否节点，则I(N0)=，即已归结为空子句□。举例如下：S={P,¬P∨Q,¬P∨¬Q}第4章消解法86消解法的完备性(2)重复上述语义树的倒塌过程，直到语义树仅由提升引理归结过程与语义树的倒塌过程是一致的进一步推广：由基例间(语义树对应的形式)可作归结，到实现子句间可作归结：即常量子句到变量子句的归结/于是得到提升引理[提升引理]若C1’和C2’分别是子句C1和C2的例子句，C’是C1’和C2’的归结式，则存在C1和C2的一个归结式C，使得C’是C的例子句第4章消解法87提升引理归结过程与语义树的倒塌过程是一致的第4章消解法87消解法完备性定理(1)简述完备性定理的证明过程：必要性：存在S到□的归结过程，□是S的逻辑推论，由合理性定理知S是不可满足的充分性：S不可满足，由Herbrand定理知存在有限封闭语义树，必有二叉树中2个兄弟节点均为否节点，即使某2个S的基例为假 该2个基例必可作归结(有互补原子)，则归结式使其父节点成为否节点(使归结式为假)第4章消解法88消解法完备性定理(1)简述完备性定理的证明过程：第4章消解消解法完备性定理(2)将归结式并入S，则该父节点是并集的否节点，因此引起语义树的倒塌重复上述过程至语义树倒塌为只剩根节点且为否节点，说明S∪{R’,...}有限集必包含□。即存在S到□的基例归结过程由提升引理知必存在S到□的子句归结过程 ★关于消解法完备性的一个证明(Robinson)见教材p230~231第4章消解法89消解法完备性定理(2)将归结式并入S，则该父节点是并集的否节消解法正确性的证明过程 存在S消解为空的过程 存在有限封闭语义树(倒塌)Herbrand解释不可满足子句集S不可满足公式G=A∧﹁B(﹁(A→B))[子句集合]是不可满足的A→B是有效的第4章消解法定理SHerbrand定理完备性定理反证法90消解法正确性的证明过程 存在S消解为空的过程 第4章人工智能原理

第4章消解法

91人工智能原理

第4章消解法1

本章内容

4.1消解法的基本思想

4.2消解法

4.3消解策略

4.4Herbrand定理

参考书目第4章消解法92 本章内容

4.1消解法的基本思想

4.24.1消解法的基本思想第4章消解法934.1消解法的基本思想第4章消解法3消解法的基本思想从第3章逻辑系统中可知，逻辑推理必须考虑其有效性(即∑|=A)，即对论域中的任何赋值都能保证公式为真从有效性和可满足性的关系可知，有效性等价于其否命题的不可满足性证明一个逻辑公式的有效性就是证明其公式的非的不可满足性(恒为假)这样就引出了消解法，其基本思想就是反证法第4章消解法94消解法的基本思想从第3章逻辑系统中可知，逻辑推理必须考虑其有消解法基本思想:反证法即：要证命题(理解为经典逻辑的公式)A恒为真，等价于证﹁A恒为假从语义上解释，恒为假就是不存在一个论域上的一个赋值(可称为解释)，使﹁A为真，即对所有的论域上的所有赋值，﹁A均为假但是，论域本身和解释有无穷多个，不可能一一验证第4章消解法95消解法基本思想:反证法即：要证命题(理解为经典逻辑的公式)A基本思想(1)Herbrand提出：从所有解释当中选出一种有代表性的解释，并严格证明一旦命题在代表性解释中为假，则在所有解释中为假Herbrand定义了这样的论域和代表性解释，称为Herbrand论域(H论域)和Herbrand解释(H解释)后面会看到：公式A(无前束范式)是不可满足的，当且仅当A(通过子句集)在所有Herbrand赋值下都取假值第4章消解法96基本思想(1)Herbrand提出：从所有解释当中选出一种有基本思想(2)这样，在证假(不可满足)的意义上使公式与子句集的语义解释等价、并与H解释等价，作为消解法的开端引入语义树，让所有解释都展现在语义树上，以便找到H解释。最后在改进寻找解释算法的复杂性中发现了消解式，从而构成了消解法的完整理论基础消解也叫归结，本章混用这两个称呼第4章消解法97基本思想(2)这样，在证假(不可满足)的意义上使公式与子句集4.2消解法

4.2.1公式到子句集的转换

4.2.2合一算法

4.2.3消解式

4.2.4消解法的实施第4章消解法984.2消解法

4.2.1公式到子句集的转换

4.2消解法的形式消解法举例：此时只要使用单文字删除规则就可以推出结论Q。但是如果子句中包含变量，则常常必须经过变量置换才能进行消解第4章消解法99消解法的形式消解法举例：第4章消解法9归结规则归结—两个互补文字消去单元归结规则—一个子句和一个文字进行互补文字消去全归结规则—两个子句中消去互补文字第4章消解法100归结规则归结—两个互补文字消去第4章消解法10公式与子句集的等价有定理S：给定公式A及相应的子句集S，则A是不可满足的当且仅当S是不可满足的实现消解法的基础是把参与推理的每个公式都转化为子句集/通过逐步对消子句集合中互补的文字(即L和﹁L)而最终得到一个空子句□，证明原来的公式是不可满足的第4章消解法101公式与子句集的等价有定理S：给定公式A及相应的子句集S，则A消解法证明的步骤证明一个公式A在给定论域下恒为真，也就是要证明﹁A恒为假将﹁A转化为一个子句集，集合中元素为原子公式或其析取/通过其中正负原子公式的合并(此时恒为真，对证假不起作用，因此消去)/最后集合为空，说明是不可满足的，即恒为假通常形式：证明﹁(A→B)为假即A∧﹁B为假，也即对应子句集归结为空子句第4章消解法102消解法证明的步骤证明一个公式A在给定论域下恒为真，也就是要证消解法证明的步骤写出谓词关系公式用反演法写出谓词表达式SKOLEM标准型子句集S对S中可消解的字句进行消解（先进行合一置换）消解式仍放入S中，反复消解过程得到空字句得证103消解法证明的步骤写出谓词关系公式134.2.1公式到子句集的转换首先复习几个定义：文字(literal)：正原子公式和负原子公式称为文字，同一原子公式的正和负称为互补的子句(clause)：文字的析取称为子句合取范式：形如A1∧A2∧…∧An的公式，其中A1～An均为子句前束范式：形如(Q1x1…Qnxn)M(x1…xn)的公式，M中不再含有量词，Q是量词Skolem标准形：在前束范式中消去存在量词后得到的公式第4章消解法1044.2.1公式到子句集的转换首先复习几个定义：第4章消解消去存在量词消去存在量词的步骤：(1)若存在量词不在任何全称量词之后，则公式中被存在量词量化的变量以某个不同于公式中任何其他常量名字的常量c代替，并消去存在量词；(2)若存在量词在k个全称量词之后，则公式中被存在量词量化的变量用被前k个全称量词量化的变量x1～xk的某个函数f(x1～xk)的形式代替，f的名字不同于公式中任何其他函数的名字，但对函数形式没有要求；然后消去存在量词/函数f称为Skolem函数第4章消解法105消去存在量词消去存在量词的步骤：第4章消解法15公式转化为子句集的步骤(1)公式A化为子句集S，其实现步骤共9步，如下：(1)消去等价和蕴含符号：蕴含转化为析取(2)将否定符号转移到每个谓词之前：应用狄摩根定律(3)变量标准化：约束变量各不相同(4)公式化为前束型：全部存在量词和全称量词移到公式的最前面/得到的两部分称为前缀和母式第4章消解法106公式转化为子句集的步骤(1)公式A化为子句集S，其实现步骤共公式转化为子句集的步骤(2)(5)消去存在量词：存在量词不受全称量词约束，则变量用常量替换/如果存在量词受全称量词约束，则使用Skolem函数替换相应变量——得到Skolem标准形(6)母式化为合取范式：外层连接符全部是合取，里层连接符全部为析取(7)去掉所有全称量词(8)母式化为子句集：每个合取项间的合取符号(∧)用逗号代替，即得子句集(9)子句变量标准化：每个子句中的变量各不相同第4章消解法107公式转化为子句集的步骤(2)(5)消去存在量词：存在量词不受4.2.2合一算法[定义]置换(或代换)：设x1～xn是n个变量，且各不相同，t1～tn是n个项(常量、变量、函数)，ti≠xi，则有限序列{t1/x1,t2/x2…tn/xn}称为一个置换置换可以作用于谓词公式，也可以作用于项。置换θ={t1/x1,t2/x2…tn/xn}作用于谓词公式E就是将E中变量xi均以ti代替，其结果用E表示/作用于项的含义相同第4章消解法1084.2.2合一算法[定义]置换(或代换)：设x1～xn是n关于置换例：={a/x,f(b)/y,u/z}E=P(x,y,z) t=g(x,y)E=P(a,f(b),u) t=g(a,f(b))[定义]置换乘积(合成)：设和是2个置换，则先后作用于公式或项，称为置换乘积，用表示(E)一般来说，置换乘积的结合律成立，即()=()，但交换律不成立第4章消解法109关于置换例：={a/x,f(b)/y,u/z}第4章合一置换[定义]合一置换：设有一组谓词公式{E1～Ek}和置换，使E1=E2=…=Ek，则称为合一置换，E1～Ek称为可合一的。合一置换也叫通代[定义]最一般合一置换(最广通代)：如果和都是公式组{E1～Ek}的合一置换，且有置换存在，使得=，则称为公式组{E1～Ek}的最一般合一置换，记为mgu(mostgeneralunification)第4章消解法110合一置换[定义]合一置换：设有一组谓词公式{E1～Ek}和置分歧集在介绍mgu求解算法之前，首先说明什么是分歧集

/合一的过程就是消除分歧[定义]分歧集(不一致集)：设W是一个非空谓词集，从左至右逐个比较W中的符号，如果在第i(i1)个符号处W中各谓词第一次出现分歧(即至少存在Ej和Ek在第i个符号处不一样，而在i之前各谓词符号均一样)，则全体谓词的第i个符号构成了W的分歧集D。分歧集性质：分歧集的出现处一定是谓词或项的开始处/求最广合一置换只考察项的分歧第4章消解法111分歧集在介绍mgu求解算法之前，首先说明什么是分歧集/合mgu求解算法求mgu算法(合一算法)设W是谓词组，表示空置换(即置换序列为空)，则算法如下：(1)k=0，W0=W，0=；(2)如果Wk中各谓词完全一样，则算法结束，k是W的mgu，否则求Wk的分歧集Dk；(3)若Dk含变量xk以及项tk的首符号且xk在tk中不出现，则继续执行算法，否则W的mgu不存在，算法停止；(4)令k+1=k{tk/xk}，Wk+1=Wk{tk/xk}；(5)k=k+1，转(2)第6章消解法112mgu求解算法求mgu算法(合一算法)第6章消解法22mgu存在条件mgu存在的条件：如果有限谓词组W是可合一的，则上述算法一定成功结束并给出其存在求mgu的预置条件：应把所有谓词中的变量换成不同名字的变量。(不过，这在将公式化为子句集时已经完成。)第4章消解法113mgu存在条件mgu存在的条件：如果有限谓词组W是可合一的，mgu求解例子(1)例1：求W={P(a,x,f(g(y))),P(z,f(a),f(u))}的mgu(1)0=，W0=W，D0={a,z}(2)1=0{a/z}={a/z}，W1=W01={P(a,x,f(g(y))),P(a,f(a),f(u))}，D1={x,f(a)}(3)2=1{f(a)/x}={a/z,f(a)/x}，W2=W12={P(a,f(a),f(g(y))),P(a,f(a),f(u))}，D2={g(y),u}(4)3=2{g(y)/u}={a/z,f(a)/x,g(y)/u}，W3=W23={P(a,f(a),f(g(y))),P(a,f(a),f(g(y)))},D3=此时W已合一，mgu=3={a/z,f(a)/x,g(y)/u} ★第4章消解法114mgu求解例子(1)例1：求W={P(a,x,f(g(ymgu求解例子(2)例2：求W={P(x,x),P(x,f(x))}的mgu首先换名：W={P(x,x),P(y,f(y))}(1)0=，W0=W，D0={x,y}(2)1={x/y}，W1={P(x,x),P(x,f(x))}，D1={x,f(x)}(3)2不存在，因为f(x)中含有变量x。故W的mgu不存在。★第4章消解法115mgu求解例子(2)例2：求W={P(x,x),P(x,4.2.3消解式[定义]文字合并规则：若子句C含有n(n>1)个相同的文字(也称为句节)，则删去其中的n-1个，结果以[C]表示。[定义]因子：若子句C中的多个文字具有mgu，则[C]称为C的一个因子。当[C]为单文字时称为C的单因子通过取因子可以简化一个子句。这是因为取因子之后，子句C中可能出现相同的文字，而根据文字合并规则就可以删除重复部分第4章消解法1164.2.3消解式[定义]文字合并规则：若子句C含有n(n>例子：C=P(x,a)∨P(b,y)∨Q(x,y,c)，={b/x,a/y}则[C]=[P(b,a)∨P(b,a)∨Q(b,a,c)]=P(b,a)∨Q(b,a,c)117例子：27二元消解式[定义]二元消解式：设C1、C2是无公共变量的子句，分别含文字L1、L2，而L1和L2有mgu，则子句R(C1,C2)=[(C1L1)∨(C2L2)] 称为C1和C2的二元消解式，其中(C1L1)和(C2L2)分别表示从C1、C2删去L1、L2所余部分。L1和L2称为被消解的文字，C1、C2称为父子句第4章消解法118二元消解式[定义]二元消解式：设C1、C2是无公共变量的子句二元消解式例子例子： 设C1=P(x)∨Q(x),C2=P(g(y))∨Q(b)∨R(x)，则C1和C2有2个二元消解式(一个消P，一个消Q) 如果取={g(y)/x}，得R(C1,C2)=Q(g(y))∨Q(b)∨R(g(y)) 如果取={b/x}，得R(C1,C2)=P(b)∨P(g(y))∨R(b)★注意：求消解式不能同时消去2个互补对文字，如同时消去P和P、Q和Q，那样所得结果就不是C1,C2的逻辑结果了第4章消解法119二元消解式例子例子：第4章消解法29子句的二元消解式子句的二元消解式：以下4种二元消解式都是子句C1和C2的二元消解式：

(1)C1和C2的二元消解式；

(2)C1的一个因子(即经过取因子处理)和C2的二元消解式；

(3)C1和C2的一个因子的二元消解式；

(4)C1的一个因子和C2的一个因子的二元消解式第4章消解法120子句的二元消解式子句的二元消解式：以下4种二元消解式都是子句4.2.4消解法的实施消解法的实施：为证├A→B，则建立G=A∧﹁B(﹁(A→B))，再求出G对应的子句集S，进而只需证明S是不可满足的为证S的不可满足，只要对S中可以消解的子句求消解式，并将消解式(新子句)加入S中，反复进行这样的消解过程直到产生一个空子句□第4章消解法1214.2.4消解法的实施消解法的实施：为证├A→B，则建立G消解的注意事项1.谓词的一致性，P()与Q()，不可以2.常量的一致性，P(a,…)与P(b,…)，不可以；但是P(a,…)与P(x,…)，可以3.变量与函数，P(a,x,…)与P(x,f(x),…)，不可以；但是P(a,x,…)与P(x,f(y)…)，可以4.不能同时消去两个互补对5.先进行内部简化（置换、合并）122消解的注意事项1.谓词的一致性，P()与Q()，不可以消解法举例“快乐学生”问题假设：任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可以通过所有考试，张不肯学习但他是幸运的，任何幸运的人都能获奖。求证：张是快乐的。证明过程：所有假设表示为一个子句集，加入结论的否定以后进行消解第4章消解法123消解法举例“快乐学生”问题第4章消解法33第4章消解法124第4章消解法34第4章消解法125第4章消解法35第4章消解法126第4章消解法364.3消解策略

4.3.1

常用消解策略

4.3.2支持集消解

4.3.3有序消解策略

4.3.4消解法举例第4章消解法1274.3消解策略

4.3.1常用消解策略

4.3.2消解过程的计算复杂性定理证明的过程就是在子句集S中不断求消解式，直到生成一个空子句□现在涉及到求