哈工大人工智能课件chpt4

人工智能原理第4章消解法本章内容4.1消解法的基本思想4.2消解法4.3消解策略4.4Herbrand定理参考书目第4章消解法4.1消解法的基本思想第4章消解法4消解法的基本思想•从第3章逻辑系统中可知，逻辑推理必须考虑其有效性(即∑|=A)，即对论域中的任何赋值都能保证公式为真•从有效性和可满足性的关系可知，有效性等价于其否命题的不可满足性•证明一个逻辑公式的有效性就是证明其公式的非的不可满足性(恒为假)•这样就引出了消解法，其基本思想就是反证法第4章消解法5消解法基本思想:反证法•即：要证命题(理解为经典逻辑的公式)A恒为真，等价于证﹁A恒为假•从语义上解释，恒为假就是不存在一个论域上的一个赋值(可称为解释)，使﹁A为真，即对所有的论域上的所有赋值，﹁A均为假•但是，论域本身和解释有无穷多个，不可能一一验证第4章消解法6基本思想(1)•Herbrand提出：从所有解释当中选出一种有代表性的解释，并严格证明一旦命题在代表性解释中为假，则在所有解释中为假•Herbrand定义了这样的论域和代表性解释，称为Herbrand论域(H论域)和Herbrand解释(H解释)•后面会看到：公式A(无前束范式)是不可满足的，当且仅当A(通过子句集)在所有Herbrand赋值下都取假值第4章消解法7基本思想(2)•这样，在证假(不可满足)的意义上使公式与子句集的语义解释等价、并与H解释等价，作为消解法的开端•引入语义树，让所有解释都展现在语义树上，以便找到H解释。•最后在改进寻找解释算法的复杂性中发现了消解式，从而构成了消解法的完整理论基础•消解也叫归结，本章混用这两个称呼第4章消解法4.2消解法4.2.1公式到子句集的转换4.2.2合一算法4.2.3消解式4.2.4消解法的实施第4章消解法9消解法的形式•消解法举例：•此时只要使用单文字删除规则就可以推出结论Q。但是如果子句中包含变量，则常常必须经过变量置换才能进行消解第4章消解法)(QPQPPS10归结规则•归结—两个互补文字消去•单元归结规则—一个子句和一个文字进行互补文字消去•全归结规则—两个子句中消去互补文字1111.........kiiikllmmlllll第4章消解法11111111..................knijiikjjnllmmlmllllmmmm11公式与子句集的等价•有定理S：给定公式A及相应的子句集S，则A是不可满足的当且仅当S是不可满足的•实现消解法的基础是把参与推理的每个公式都转化为子句集/通过逐步对消子句集合中互补的文字(即L和﹁L)而最终得到一个空子句□，证明原来的公式是不可满足的第4章消解法12消解法证明的步骤•证明一个公式A在给定论域下恒为真，也就是要证明﹁A恒为假•将﹁A转化为一个子句集，集合中元素为原子公式或其析取/通过其中正负原子公式的合并(此时恒为真，对证假不起作用，因此消去)/最后集合为空，说明是不可满足的，即恒为假•通常形式：证明﹁(A→B)为假即A∧﹁B为假，也即对应子句集归结为空子句第4章消解法13消解法证明的步骤1.写出谓词关系公式2.用反演法写出谓词表达式3.SKOLEM标准型4.子句集S5.对S中可消解的字句进行消解（先进行合一置换）6.消解式仍放入S中，反复消解过程7.得到空字句8.得证144.2.1公式到子句集的转换•首先复习几个定义：•文字(literal)：正原子公式和负原子公式称为文字，同一原子公式的正和负称为互补的•子句(clause)：文字的析取称为子句•合取范式：形如A1∧A2∧…∧An的公式，其中A1～An均为子句•前束范式：形如(Q1x1…Qnxn)M(x1…xn)的公式，M中不再含有量词，Q是量词•Skolem标准形：在前束范式中消去存在量词后得到的公式第4章消解法15消去存在量词•消去存在量词的步骤：(1)若存在量词不在任何全称量词之后，则公式中被存在量词量化的变量以某个不同于公式中任何其他常量名字的常量c代替，并消去存在量词；(2)若存在量词在k个全称量词之后，则公式中被存在量词量化的变量用被前k个全称量词量化的变量x1～xk的某个函数f(x1～xk)的形式代替，f的名字不同于公式中任何其他函数的名字，但对函数形式没有要求；然后消去存在量词/函数f称为Skolem函数第4章消解法16公式转化为子句集的步骤(1)•公式A化为子句集S，其实现步骤共9步，如下：(1)消去等价和蕴含符号：蕴含转化为析取(2)将否定符号转移到每个谓词之前：应用狄摩根定律(3)变量标准化：约束变量各不相同(4)公式化为前束型：全部存在量词和全称量词移到公式的最前面/得到的两部分称为前缀和母式第4章消解法17公式转化为子句集的步骤(2)(5)消去存在量词：存在量词不受全称量词约束，则变量用常量替换/如果存在量词受全称量词约束，则使用Skolem函数替换相应变量——得到Skolem标准形(6)母式化为合取范式：外层连接符全部是合取，里层连接符全部为析取(7)去掉所有全称量词(8)母式化为子句集：每个合取项间的合取符号(∧)用逗号代替，即得子句集(9)子句变量标准化：每个子句中的变量各不相同第4章消解法184.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章消解法19关于置换•例：={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章消解法20合一置换•[定义]合一置换：设有一组谓词公式{E1～Ek}和置换，使E1=E2=…=Ek，则称为合一置换，E1～Ek称为可合一的。合一置换也叫通代•[定义]最一般合一置换(最广通代)：如果和都是公式组{E1～Ek}的合一置换，且有置换存在，使得=，则称为公式组{E1～Ek}的最一般合一置换，记为mgu(mostgeneralunification)第4章消解法21分歧集•在介绍mgu求解算法之前，首先说明什么是分歧集/合一的过程就是消除分歧•[定义]分歧集(不一致集)：设W是一个非空谓词集，从左至右逐个比较W中的符号，如果在第i(i1)个符号处W中各谓词第一次出现分歧(即至少存在Ej和Ek在第i个符号处不一样，而在i之前各谓词符号均一样)，则全体谓词的第i个符号构成了W的分歧集D。•分歧集性质：分歧集的出现处一定是谓词或项的开始处/求最广合一置换只考察项的分歧第4章消解法22mgu求解算法•求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章消解法23mgu存在条件•mgu存在的条件：如果有限谓词组W是可合一的，则上述算法一定成功结束并给出其存在•求mgu的预置条件：应把所有谓词中的变量换成不同名字的变量。(不过，这在将公式化为子句集时已经完成。)第4章消解法24mgu求解例子(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=W01={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=W12={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=W23={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章消解法25mgu求解例子(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章消解法264.2.3消解式•[定义]文字合并规则：若子句C含有n(n1)个相同的文字(也称为句节)，则删去其中的n-1个，结果以[C]表示。•[定义]因子：若子句C中的多个文字具有mgu，则[C]称为C的一个因子。当[C]为单文字时称为C的单因子•通过取因子可以简化一个子句。这是因为取因子之后，子句C中可能出现相同的文字，而根据文字合并规则就可以删除重复部分第4章消解法27•例子：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)28二元消解式•[定义]二元消解式：设C1、C2是无公共变量的子句，分别含文字L1、L2，而L1和L2有mgu，则子句R(C1,C2)=[(C1L1)∨(C2L2)]称为C1和C2的二元消解式，其中(C1L1)和(C2L2)分别表示从C1、C2删去L1、L2所余部分。L1和L2称为被消解的文字，C1、C2称为父子句第4章消解法29二元消解式例子•例子：设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章消解法30子句的二元消解式•子句的二元消解式：以下4种二元消解式都是子句C1和C2的二元消解式：(1)C1和C2的二元消解式；(2)C1的一个因子(即经过取因子处理)和C2的二元消解式；(3)C1和C2的一个因子的二元消解式；(4)C1的一个因子和C2的一个因子的二元消解式第4章消解法314.2.4消解法的实施•消解法的实施：为证├A→B，则建立G=A∧﹁B(﹁(A→B))，再求出G对应的子句集S，进而只需证明S是不可满足的•为证S的不可满足，只要对S中可以消解的子句求消解式，并将消解式(新子句)加入S中，反复进行这样的消解过程直到产生一个空子句□第4章消解法32消解的注意事项•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.先进行内部简化（置换、合并）33消解法举例•“快乐学生”问题•假设：任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可以通过所有考试，张不肯