人工智能第三章27

13.4归结演绎推理•归结演绎推理是一种基于Robinson归结原理的机器推理技术。Robinson归结原理亦称为消解原理，是Robinson于1965年在Herbrand理论的基础上提出的一种基于逻辑的“反证法”。•在人工智能中，几乎所有的问题都可以转化为一个定理证明问题。定理证明的实质，就是要对前提P和结论Q，证明P→Q永真。•由3.2节可知，要证明P→Q永真，就是要证明P→Q在任何一个非空的个体域上都是永真的。这将是非常困难的，甚至是不可实现的。2•为此，人们进行了大量的探索，后来发现可以采用反证法的思想，把关于永真性的证明转化为关于不可满足性的证明。即要证明P→Q永真，只要能够证明P∧﹁Q是不可满足的就可以了。原因是:﹁(P→Q)⇔﹁(﹁P∨Q)⇔P∧﹁Q。•这方面最有成效的工作就是Robinson归结原理。它使定理证明的机械化成为现实。33.4归结演绎推理•3.4.1子句集及其化简•3,4.2鲁滨逊归结原理•3.4.3归结反演推理的归结策略•3.4.4用归结反演求取问题的答案43.4.3归结演绎推理的归结策略•归结演绎推理实际上就是从子句集中不断寻找可进行归结的子句对，并通过对这些子句对的归结，最终得出一个空子句的过程。由于事先并不知道哪些子句对可进行归结，更不知道通过对哪些子句对的归结能尽快得到空子句，因此就需要对子句集中的所有子句逐对进行比较，直到得出空子句为止。•这种盲目的全面进行归结的方法，不仅会产生许多无用的归结式，更严重的是会产生组核爆炸问题。因此，需要研究有效的归结策略来解决这些问题。5•目前，常用的归结策略可分为两大类，一类是删除策略，另一类是限制策略。删除策略是通过删除某些无用的子句来缩小归结范围；限制策略是通过对参加归结的子句进行某些限制，来减少归结的盲目性，以尽快得到空子句。•为了说明选择归结策略的重要性，在讨论各种常用的归结策略之前，还是先提一下广度优先策略。63.4.3归结演绎推理的归结策略1.广度优先策略•广度优先：是一种穷尽子句比较的复杂搜索方法。设初始子句集为S0，其归结过程可描述如下：(1)从S0出发，对S0中的全部子句作所有可能的归结，得到第一层归结式，把这些归结式的集合记为S1;(2)用S0中的子句与S1中的子句进行所有可能的归结，得到第二层归结式，把这些归结式的集合记为S2;(3)用S0和S1中的子句与S2中的子句进行所有可能的归结，得到第三层归结式，把这些归结式的集合记为S3;•如此继续，知道得出空子句或不能再继续归结为止。7•例3.19设有如下子句集：S={﹁I(x)∨R(x),I(a),﹁R(y)∨L(y),﹁L(a)}用宽度优先策略证明S为不可满足。宽度优先策略的归结树如下：﹁I(x)∨R(x)I(a)﹁R(y)∨L(y)﹁L(a)R(a)﹁I(x)∨L(x)﹁R(a)L(a)L(a)﹁I(a)﹁I(a)NILSS1S28•从这个例子可以看出，宽度优先策略归结出了许多无用的子句，既浪费事间，又浪费空间。但是，这种策略由一个有趣的特性，就是当问题有解时保证能找到最短归结路径。•因此，它是一种完备的归结策略。宽度优先对大问题的归结容易产生组合爆炸，但对小问题却仍是一种比较好的归结策略。93.4.3归结演绎推理的归结策略2.支持集策略•支持集策略：要求每一次参加归结的两个亲本子句中，至少应该有一个是由目标公式的否定所得到的子句或它们的后裔。•可以证明支持集策略是完备的，即当子句集为不可满足时，则由支持集策略一定能够归结出一个空子句。也可以把支持集策略看成是在宽度优先策略中引入了某种限制条件，这种限制条件代表一种启发信息，因而有较高的效率10﹁I(x)∨R(x)I(a)﹁R(y)∨L(y)﹁L(a)R(a)﹁I(x)∨L(x)L(a)L(a)﹁I(a)NIL例3.20设有如下子句集：S={﹁I(x)∨R(x),I(a),﹁R(y)∨L(y),﹁L(a)}其中，﹁I(x)∨R(x)为目标公式的否定。用支持集策略证明S为不可满足。11从上述归结过程可以看出：–各级归结式数目要比宽度优先策略生成的少，但在第二级还没有空子句。就是说这种策略限制了子句集元素的剧增，但会增加空子句所在的深度。–此外，支持集策略具有逆向推理的含义，由于进行归结的亲本子句中至少有一个与目标子句有关，因此推理过程可以看作是沿目标、子目标的方向前进的。123.4.5归结演绎推理的归结策略3.删除策略•主要想法是：归结过程在寻找可归结子句时，子句集中的子句越多，需要付出的代价就会越大。如果在归结时能把子句集中无用的子句删除掉，这就会缩小搜索范围，减少比较次数，从而提高归结效率。•常用的删除方法有以下几种（纯文字、重言式、包含）13•纯文字删除法•如果某文字L在子句集中不存在可与其互补的文字﹁L，则称该文字为纯文字。•在归结过程中，纯文字不可能被消除，用包含纯文字的子句进行归结也不可能得到空子句，因此对包含纯文字的子句进行归结是没有意义的，应该把它从子句集中删除。•对子句集而言，删除包含纯文字的子句，是不影响其不可满足性的。例如，对子句集•S={P∨Q∨R,﹁Q∨R,Q,﹁R}•其中P是纯文字，因此可以将子句P∨Q∨R从子句集S中删除。14•重言式删除法•如果一个子句中包含有互补的文字对，则称该子句为重言式。例如P(x)∨﹁P(x),P(x)∨Q(x)∨﹁P(x)都是重言式，不管P(x)的真值为真还是为假，P(x)∨﹁P(x)和P(x)∨Q(x)∨﹁P(x)都均为真。•重言式是真值为真的子句。对一个子句集来说，不管是增加还是删除一个真值为真的子句，都不会影响该子句集的不可满足性。因此，可从子句集中删去重言式。15•包含删除法•设有子句C1和C2，如果存在一个置换σ，使得C1σ⊆C2，则称C1包含于C2。例如•P(x)包含于P(y)∨Q(z)σ={x/y}•P(x)包含于P(a)σ={a/x}•P(x)包含于P(a)∨Q(z)σ={a/x}•P(x)∨Q(a)包含于P(f(a))∨Q(a)∨R(y)σ={f(a)/x}•P(x)∨Q(y)包含于P(a)∨Q(u)∨R(w)σ={a/x,u/y}•对子句集来说，把其中包含的子句删去后，不会影响该子句集的不可满足性。因此，可从子句集中删除哪些包含的子句。163.4.3归结演绎推理的归结策略4.单文字子句策略•如果一个子句只包含一个文字，则称此子句为单文字子句。单文字子句策略是对支持集策略的进一步改进，它要求每次参加归结的两个亲本子句中至少有一个子句是单文字子句。•例3.21设有如下子句集：S={﹁I(x)∨R(x),I(a),﹁R(y)∨L(y),﹁L(a)}用单文字子句策略证明S为不可满足。17•采用单文字子句策略，归结式包含的文字数将少于其亲本子句中的文字数，这将有利于向空子句的方向发展，因此会有较高的归结效率。但这种策略是不完备的，即当子句集为不可满足时，用这种策略不一定能归结出空子句。﹁I(x)∨R(x)I(a)﹁R(y)∨L(y)﹁L(a)R(a)﹁R(a)NIL183.4.3归结演绎推理的归结策略5.线形输入策略•这种策略要求每次参加归结的两个亲本子句中，至少应该有一个是初始子句集中的子句。所谓初始子句集是指开始归结时所使用的子句集。•例3.22设有如下子句集：S={﹁I(x)∨R(x),I(a),﹁R(y)∨L(y),﹁L(a)}用线性输入策略证明S为不可满足。•线性输入策略可限制生成归结式的数目，具有简单和高效的优点。但是，这种策略也是一种不完备的策略。19﹁I(x)∨R(x)I(a)﹁R(y)∨L(y)﹁L(a)R(a)﹁I(x)∨L(x)﹁R(a)﹁I(a)L(a)L(a)﹁I(a)NIL•例如，子句集S={Q(u)∨P(a),﹁Q(w)∨P(w),﹁Q(x)∨﹁P(x),Q(y)∨﹁P(y)}从S出发很容易找到一棵归结反演树，但却不存在线性输入策略的归结反演树。203.4.3归结演绎推理的归结策略6.祖先过滤策略•这种策略与线性输入策略有点相似，但是，放宽了对子句的限制。每次参加归结的两个亲本子句，只要满足以下两个条件中的任意一个就可进行归结：(1)两个亲本子句中至少有一个是初始子句集中的子句(2)如果两个亲本子句都不是初始子句集中的子句，则一个子句应该是另一个子句的先辈子句。•所谓一个子句(例如C1)是另一个子句(例如C2)的先辈子句是指C2是由C1与别的子句归结后得到的归结式。21•例3.23设有如下子句集：S={﹁Q(x)∨﹁P(x),Q(y)∨﹁P(y)，﹁Q(w)∨P(w),Q(a)∨P(a)}用祖先过滤策略证明S为不可满足•证明：从S出发，按祖先过滤策略归结过程如下图所示。•可以证明祖先过滤策略也是完备的。•在实际应用中，可以把几种策略结合起来使用。总之，在选择归结反演策略时，主要应考虑其完备性和效率问题。22﹁Q(x)∨﹁P(x)Q(y)∨﹁P(y)﹁P(x)﹁Q(w)∨P(w)﹁Q(w)Q(a)∨P(a)P(a)NIL233.4.4用归结反演求取问题的答案•归结原理除了可用于定理证明外，还可用来求取问题答案，其思想与定理证明相似。•其一般步骤为：(1)把问题的已知条件用谓词公式表示出来，并化为相应的子句集；(2)把问题的目标的否定用谓词公式表示出来，并化为子句集；24(3)对目标否定子句集中的每个子句，构造该子句的重言式（即把该目标否定子句和此目标否定子句的否定之间再进行析取所得到的子句），用这些重言式代替相应的目标否定子句式，并把这些重言式加入到前提子句集中，得到一个新的子句集(4)对这个新的子句集，应用归结原理求出其证明树，这时证明树的根子句不为空，称这个证明树为修改的证明树；(5)用修改证明树的根子句作为回答语句，则答案就在此根子句中。25例3.24已知：“张和李是同班同学，如果x和y是同班同学，则x的教室也是y的教室，现在张在302教室上课。”问：“现在李在哪个教室上课？”•解：首先定义谓词：C(x,y)x和y是同班同学；At(x,u)x在u教室上课。•把已知前提用谓词公式表示如下：C(zhang,li)(∀x)(∀y)(∀u)(C(x,y)∧At(x,u)→At(y,u))At(zhang,302)•把目标的否定用谓词公式表示如下：﹁(∃v)At(li,v)26•把上述公式化为子句集：{C(zhang,li)，﹁C(x,y)∨﹁At(x,u)∨At(y,u)，At(zhang,302)}•把目标的否定化成子句式，并用重言式﹁At(li,v)∨At(li,v)代替之。•把此重言式加入前提子句集中，得到一个新的子句集，对这个新的子句集，应用归结原理求出其证明树•其求解过程如下图所示。•该证明树的根子句就是所求的答案，即“李明在302教室”。27﹁At(li,v)∨At(li,v)﹁C(x,y)∨﹁At(x,u)∨At(y,u)At(li,v)∨﹁C(x,li)∨﹁At(x,v)C(zhang,li)﹁At(zhang,v)∨At(li,v)At(zhang,302)At(li,302){li/y,v/u}{Zhang/x}{302/v}