人工智能原理第5章消解法

人工智能原理第4章消解法本章内容4.1消解法的基本思想4.2Herbrand定理4.3消解法4.4消解策略参考书目第4章消解法4.1消解法的基本思想第4章消解法4消解法的基本思想•从第3章逻辑系统中可知，逻辑推理必须考虑其有效性(即∑|=A)，即对论域中的任何赋值都能保证公式为真•由可靠性定理知：逻辑系统中任何正确的推理，都要具有“如果∑|—A则∑|=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.2Herbrand定理4.2.1公式到子句集的转换4.2.2Herbrand论域和解释4.2.3语义树4.2.4Herbrand定理4.2.5不可满足基子句集第4章消解法9证明的步骤•证明一个公式A在给定论域下恒为真，也就是要证明﹁A恒为假•将﹁A转化为一个子句集，集合中元素为原子公式或其析取/通过其中正负原子公式的合并(此时恒为真，对证假不起作用，因此消去)/最后集合为空，说明是不可满足的，即恒为假•通常形式：证明﹁(A→B)为假即A∧﹁B为假，也即对应子句集归结为空子句•首先介绍基本术语复习和公式到子句集的转换第4章消解法104.2.1公式到子句集的转换•首先复习几个定义：•文字(literal)：正原子公式和负原子公式称为文字，同一原子公式的正和负称为互补的。•子句(clause)：文字的析取称为子句。•合取范式：形如A1∧A2∧…∧An的公式，其中A1～An均为子句。•前束范式：形如(Q1x1…Qnxn)M(x1…xn)的公式，M中不再含有量词。•Skolem标准形：在前束范式中消去存在量词后得到的公式第4章消解法11消去存在量词•消去存在量词的步骤：(1)若存在量词不在任何全称量词之后，则公式中被存在量词量化的变量以某个不同于公式中任何其他常量名字的常量c代替，并消去存在量词；(2)若存在量词在k个全称量词之后，则公式中被存在量词量化的变量用被前k个全称量词量化的变量x1～xk的某个函数f(x1～xk)的形式代替，f的名字不同于公式中任何其他函数的名字，但对函数形式没有要求；然后消去存在量词/函数f称为Skolem函数第4章消解法12公式转化为子句集的步骤(1)•公式A化为子句集S，其实现步骤共9步，如下：(1)消去等价和蕴含符号：蕴含转化为析取(2)将否定符号转移到每个谓词之前：应用狄摩根定律(3)变量标准化：约束变量各不相同(4)消去存在量词：存在量词不受全称量词约束，则变量用常量替换/如果存在量词受全称量词约束，则使用Skolem函数替换相应变量——得到Skolem标准形第4章消解法13公式转化为子句集的步骤(2)(5)公式化为前束型：全部全称量词移到公式的最前面/得到的两部分称为前缀和母式(6)母式化为合取范式：外层连接符全部是合取，里层连接符全部为析取(7)去掉所有全称量词(8)母式化为子句集：每个合取项间的合取符号(∧)用逗号代替，即得子句集(9)子句变量标准化：每个子句中的变量各不相同第4章消解法14公式与子句集的等价•实现消解法的基础是把参与推理的每个公式都转化为子句集/通过逐步对消子句集合中互补的文字(即L和﹁L)而最终得到一个空子句□，证明原来的公式是不可满足的•反证法定理：给定公式A及相应的子句集S，则A是不可满足的当且仅当S是不可满足的•使用子句集进行消解法推理，其过程是完备的—即如果公式X是子句集S的逻辑推论，则X可以从S中推出第4章消解法154.2.2Herbrand论域和解释•Herbrand论域定义•Herbrand论域(H论域)：设S为子句集，H0是S中子句所含的全体常量集，若S中子句不含常量，则任选一常量a令H0={a}。对i≥1令Hi=Hi-1∪{f(t1,…tn)|n≥1f是S中的任一函数符号，t1,…tn是Hi-1中的元素则Hi称为S的i阶常量集，H∞称为S的Herbrand论域，其元素称为基项。第4章消解法0iiHH16H论域例子例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,dH∞}★第4章消解法17Herbrand原子集•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章消解法},1|)({1HtnttPHin18Herbrand解释(1)•Herbrand解释是一种语义结构•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∞第4章消解法19Herbrand解释(2)(5)S中的每个谓词Pn对应于一个映射H∞×H∞×…×H∞(n个)→{T,F}•该定义表明，一旦给定一个子句集，其H解释基本就确定了/唯一留下的自由度是由谓词P代表的映射即~H到{T,F}的映射。•~H可以分解如下：~H=~H1∪~H2h~H1，v(h)=T；h~H2，v(h)=F这样，一旦给出~H1或~H2，则H解释就完全确定了，通常是给出~H1第4章消解法20H解释例子•例子：•在例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基(原子集)有n个元素(谓词)，则谓词取不同真值的组合有2n种，也即2n不同种解释第4章消解法214.2.3语义树•语义树的表示：要寻找S的H解释的不可满足性质，可以把所有H解释展现在一棵语义树上，然后观察S对应的各个原子公式的真假值。这是一种很直观的研究方式，称为语义树方法•设S={P,Q,R}，则H∞={a}，~H={P(a),Q(a),R(a)}(只有一个常量a，在语义树中可省略)•因为是二值逻辑，研究每个基原子(即S的原子公式)的取值可以通过原子及其否定(即文字)来观察/构造如下二叉形式的语义树第4章消解法22语义树示例•通常用I(Ni)表示从根节点到节点Ni分枝上所标记的所有文字的并集。如：I(N22)={P,Q}，I(N35)={P,Q,R}第4章消解法N0PPN11N12QQQQN21N22N23N24RRN31N32N33N34N35N36N37N3823语义树定义(1)•子句集S语义树的定义•[定义]设子句集S，对应H基为~H，S的语义树ST定义如下：(1)ST是一棵树；(2)ST的节点均不带标记，而边的标记是基原子且不包含其中的变量(边的标记可能不止一个，用逗号分割)；(3)从每个非叶节点只生成有限个边L1Ln，令Qi是每个Li的标记的合取，则Q1Q2…Qn为永真；(4)从根节点到任一叶子节点的路径上，所有边的标记的并集中不含重复的基原子，也不含互补的基原子第4章消解法24语义树定义(2)•[定义]规范语义树：如果一棵语义树的每条边的标记均为一个原子公式•[定义]完备语义树：如果一棵语义树从根节点到任一叶节点的路径上所有边标记的并集中包含子句集中每个原子或其负原子，则该语义树称为完备的(完全的)第4章消解法25语义树定义(3)•对于给定的S，其语义树一般都不唯一。下图中语义树和前图中的语义树对应于同一个H基。这两个图的语义树都是完备的第4章消解法P,RPRQQQ,RQRPPRRQQQQQQ26语义树定义(4)•因为一般H基是个无穷集合，所以其对应的语义树也是无限的•因为在完备语义树的每一条路径上都有S的全部原子(或负原子)，所以对这些原子公式的真值判定就能决定S的一个解释•对于有限完备语义树来说，如果N是一个叶节点，则I(N)便是S的一个解释/这样，S的不可满足性就与完备语义树路径的真值计算联系起来第4章消解法27语义树定义(5)[定义]基例：如果S的某个子句C中所有变量符号均以S的H域的元素(常量)代入时，所得的子句C’称为C的一个基例[定义]否节点：如果语义树节点N的从根节点到N的路径I(N)使S的某个子句的某个基例为假，而其父辈节点不能判断此事实(即I(N)是使基例为假的最小路径)，则称N为否节点(或失败节点)[定义]封闭语义树：如果一棵完全语义树的每个分枝上都有一个否节点，则称为封闭语义树第4章消解法28封闭语义树例子(1)•例：设子句集S={﹁P(x)∨Q(x),P(f(x)),﹁Q(f(x))}则H∞={a,f(a),f(f(a)),…}={P(a),Q(a),P(f(a)),Q(f(a)),…}•包括3个子句:﹁P(x)∨Q(x),P(f(x),﹁Q(f(x))•其封闭语义树如下图所示第4章消解法29封闭语义树例子(2)第4章消解法●N0P(a)﹁P(a)●N1/1●N1/2Q(a)﹁Q(a)Q(a)﹁Q(a)●N2/1★N2/2●N2/3●N2/4P(f(a))P(f(a))●N3/1★N3/2●N3/5★N3/6●N3/7★N3/8Q(f(a))Q(f(a))★★★★★★N4/1N4/2N4/9N4/10N4/13N4/1430封闭语义树例子(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章消解法31有限封闭语义树•上例说明，从不可满足的角度来说，对于无限完备语义树只需搜索到一个否节点，则