第4章推理技术(人工智能)46

2012-5-814.1归结演绎推理4.3产生式系统4.5不确定性推理第4章推理技术引入：归结演绎定理证明的实质是证明F1∧F2∧…∧Fn→W的永真性。其证明方法可分为二类：一是直接证明F1∧F2∧…∧Fn→W为永真，即演绎法；二是间接证明(F1∧F2∧…∧Fn→W)为永假，即反证法。20世纪60年代，人们把研究的注意力集中在证明永假性，即证明F1∧F2∧…∧Fn∧W的永假性，这实际上就是要证明{F1,F2,…,Fn}∪{W}是一个矛盾集，也就是证明F1∧F2∧…∧Fn和W是不可满足的。J.Herbrand和Robinson在这个方向上先后作了卓越的研究工作。首先，由Herbrand提出的Herbrand域和Herbrand定理，为自动定理证明奠定了理论基础；然后，由Robinson提出的归结原理使自动定理证明成为可能。2012-5-82Herbrand理论证明一个谓词公式的不可满足性是困难的，这是由于个体变量论域的任意性，以及解释的个数的无限性。但是，如果一个具体的谓词公式能够找到一个比较简单的特殊的论域，使得只要在这个论域上该公式是不可满足的，便能保证该公式在任一论域上也是不可满足的，这将对不可满足性的证明是十分有益的。Herbrand首先将合式公式标准化为子句集；然后在此基础上引入Herbrand域（简记为H域），并证明只要对这个特殊域上的一切解释进行判定，就能得知子句集是否不可满足。他从理论上给出了证明子句集永假的可行性以及方法。4.1归结演绎推理Resolutiondeduction4.1.1子句集的求取定义1原子谓词公式及其否定称为文字literal，若干个文字的一个析取式称为一个子句clause，由r个文字组成的子句叫r—文字子句，1—文字子句叫单元子句，不含任何文字的子句称为空子句，记为或NIL。例如下面的析取式都是子句P∨Q∨乛RP(x,y)∨乛Q(x)p.1062012-5-83定义2对一个谓词公式G，通过以下步骤所得的子句集合S（子句集中各子句之间具有合取关系），称为G的子句集。(1)消去蕴含词→和等值词。可使用逻辑等价式：①A→B乛A∨B②AB(乛A∨B)∧(乛B∨A)(2)缩小否定词的作用范围，直到其仅作用于原子公式。可使用逻辑等价式：①乛(乛A)A②乛(A∧B)乛A∨乛B③乛(A∨B)乛A∧乛B④乛xP(x)x乛P(x)⑤乛xP(x)x乛P(x)(3)适当改名，使量词间不含同名指导变元和约束变元。(4)消去存在量词。消去存在量词，要进行变元替换。分两种情况：①若该存在量词在某些全称量词的辖域内（如：xy，则用这些全称量词指导变元的一个新的函数(未曾在公式中出现过)代替该存在量词辖域中的相应约束变元，这样的函数称为Skolem函数；②若该存在量词不在任何全称量词的辖域内，则用一个新的常量符号(未曾在公式中出现过)代替该存在量词辖域中的相应约束变元，这样的常量符号称为Skolem常量。2012-5-84(5)消去所有全称量词。(6)化公式为合取范式。可使用逻辑等价式：①A∨(B∧C)(A∨B)∧(A∨C)②(A∧B)∨C(A∨C)∧(B∨C)(7)消去合取词∧，以子句为元素组成一个集合S。子句内的文字可含有变量，这些变量被理解为隐含地受全称量词约束。(8)适当改名，使子句间无同名变元。需说明的是，在上述求子句集的过程中，当消去存在量词后，把所有全称量词都依次移到整个式子的最左边（或者先把所有量词都依次移到整个式子的最左边(得到前束范式)，再消去存在量词，即Skolemization，得到斯柯林范式），再将右部的式子化为合取范式，这时所得的式子称为原谓词公式的Skolem标准型。例如，上例中的Skolem标准型：x{［乛P(x,f(x))∨Q(x,g(x))］∧［乛P(y,f(y))∨乛R(y,g(y))］}2012-5-85例求下面谓词公式的子句集x{yP(x,y)→乛y［Q(x,y)→R(x,y)］}解由步(1)得x{乛yP(x,y)∨乛y［乛Q(x,y)∨R(x,y)］}由步(2)得x{y乛P(x,y)∨y［Q(x,y)∧乛R(x,y)］}由步(3)得x{y乛P(x,y)∨z［Q(x,z)∧乛R(x,z)］}由步(4)得x{乛P(x,f(x))∨［Q(x,g(x))∧乛R(x,g(x))］}由步(5)得乛P(x,f(x))∨［Q(x,g(x))∧乛R(x,g(x))］由步(6)得［乛P(x,f(x))∨Q(x,g(x))］∧［乛P(x,f(x))∨乛R(x,g(x))］由步(7)得［乛P(x,f(x))∨Q(x,g(x))］∧［乛P(y,f(y))∨乛R(y,g(y))］由步(8)得{乛P(x,f(x))∨Q(x,g(x)),乛P(y,f(y))∨乛R(y,g(y))}或乛P(x,f(x))∨Q(x,g(x))乛P(y,f(y))∨乛R(y,g(y))为原谓词公式的子句集。2012-5-86定理谓词公式G不可满足iff其子句集S不可满足。定理1把证明一个公式G的不可满足，转化为证明其子句集S的不可满足。注意，这并不意味着G与S间等价。由于在谓词公式G的化简过程中，为消除存在量词而引入了Skolem函数，从而使子句集S实际上只是G的一个特例。然而，可以证明G和S在永假性上是等价的，这成为建立Herbrand定理的重要基础。定义3子句集S是不可满足的unsatisfiable(orcontradictory)，当且仅当其全部（或部分）子句的合取式是不可满足的。虽然Herbrand从理论上给出了证明子句集不可满足的可行性及方法（Herbrand域的定义、Herbrand定理以及相关方法等这里从略），但在计算机上实现其证明过程却十分困难。1965年Robinson提出归结原理，这才使自动定理证明变成现实。2012-5-87归结演绎推理是基于归结原理（亦称消解原理principleofresolution）的推理方法。归结原理是由鲁滨逊(JohnAlanRobinson)于1965年首先提出。它是谓词逻辑中一个相当有效的机械化推理方法。归结原理的出现，被认为是自动推理（AR:AutomatedReasoning），特别是定理机器证明领域（Automatedtheoremproving,iscurrentlythemostwell-developedsub-fieldofAR）的重大突破。定义4设L为一个文字，则称L与乛L为互补文字complementaryliterals。定义5设C1,C2是命题逻辑中的两个子句，C1中有文字L1，C2中有文字L2，且L1与L2互补，从C1,C2中分别删除L1,L2，再将剩余部分析取起来，记构成的新子句为C12，则称C12为C1,C2的归结式（或消解式resolvent），C1,C2称为其归结式的亲本子句parentclauses，L1,L2称为消解基。例设C1=乛P∨Q∨R，C2=乛Q∨S，于是C1,C2的归结式为乛P∨R∨S命题逻辑中的归结2012-5-88例用归结原理验证：分离规则(或假言推理)：A∧(A→B)B拒取式：(A→B)∧乛B乛A链式(假言三段论)：(AB)∧(BC)(AC)解A∧(A→B)A∧(乛A∨B)B(A→B)∧乛B(乛A∨B)∧(乛B)乛A(乛A∨B)∧(乛B∨C)乛A∨CAC类似地可以验证其他推理规则也都可以用消解原理推出。这就是说，用消解原理就可以代替其他所有的推理规则。再加上这个方法的推理步骤比较机械，这就为机器推理提供了方便。例证明子句集{P∨乛Q,乛P,Q}是不可满足的。证(1)P∨乛Q(2)乛P(3)乛Q由(1),(2)(4)Q(5)□由(3),(4)2012-5-89例用归结原理证明：R是P,(P∧Q)→R,(S∨U)→Q,U的逻辑结果。证：我们先把诸前提条件化为子句形式，再把结论的非也化为子句，由所有子句得到子句集S=｛P,乛P∨乛Q∨R,乛S∨Q,乛U∨Q,U,乛R｝，然后对该子句集施行归结。由于最后推出了空子句，所以子句集S不可满足，即命题公式P∧(乛P∨乛Q∨R)∧(乛S∨Q)∧(乛U∨Q)∧U∧乛R不可满足，从而R是题设前提的逻辑结果。在一阶谓词逻辑中应用消解原理，不像命题逻辑中那样简单，因为谓词逻辑中的子句含有个体变元，这就使寻找含互否文字的子句对的操作变得复杂。例如：C1=P(x)∨Q(x)C2=P(a)∨R(y)我们需要用a替换C1中的x，两者中才有互否文字。然后才能根据命题逻辑中的消解原理，得消解式C3’=Q(a)∨R(y)所以，要在谓词逻辑中应用消解原理，一般需要对个体变元作适当的替换。p.1104.1.3含有变量的消解替换与合一（用于谓词逻辑中的归结）2012-5-810定义6一个替换/置换(Substitution)是形如｛t1/x1,t2/x2,…,tn/xn｝的有限集合，ti/xi表示用ti替换xi。其中x1,x2,…,xn是互不相同的个体变元，称为替换的分母，ti称为替换的分子；ti不同于xi，xi也不循环地出现在tj(i,j=1,2,…,n)中。若t1,t2,…,tn都是不含变元的项（称为基项），该替换称为基替换；没有元素的替换称为空替换，记作ε，表示不作替换。例如：｛a/x,g(y)/y,f(g(b))/z｝就是一个替换；而{g(y)/x,f(x)/y}则不是一个合法的替换，因为x与y出现了循环替换（x依赖y，y又依赖x）。下面我们将项、文字（原子公式及其否定）、子句等统称为表达式，没有变元的表达式称为基表达式，出现在表达式E中的表达式称为E的子表达式。定义7设=｛t1/x1,…,tn/xn｝是一个替换，E是一个表达式；对E施行替换，即把E中出现的个体变元xj(1≤j≤n)都用tj替换，记为E，所得的结果称为E在下的例(instance)。2012-5-811定义8设=｛t1/x1,…,tn/xn｝，λ=｛u1/y1,…,um/ym｝是两个替换；将集合｛t1λ/x1,…,tnλ/xn,u1/y1,…,um/ym｝中凡符合下列条件的元素删除：(1)tiλ/xi当tiλ=xi(2)ui/yi当yi∈{x1,…,xn}得到的集合仍然是一个替换，该替换称为与λ的复合或乘积，记为·λ。可以证明，替换的乘积满足结合律，即：(·λ)·u=·(λ·u)替换一般不满足交换律。替换的定义的基本要求变量替换，使两个或多个表达式一致，称合一(unification)。定义9设原子谓词公式集S={F1,F2,…,Fn}，若存在一个替换，使F1=F2=…=Fn，则称为S的一个合一者(Unifier)，称S为可合一的。一个原子公式集的合一者一般不唯一。定义10设原子公式集S的一个合一者，如果对S的任何一个合一者，都存在一个替换λ，使得=·λ则称为S的最一般的合一者(MostGeneralUnifier)，简称MGU。2012-5-812可以看出，如果能找到一个原子公式集的合一者，特别是最一般的合一者，则可使互否的文字的形式结构完全一致起来，进而达到消解的目的。谓词逻辑中的归结原理定义12设C1,C2是两个无相同变元的子句，L1,L2分别是C1,C2中的两个文字，如果L1和乛L2有最一般合一者，则子句(C1-｛L1｝)∨(C2-｛L2｝)称作C1和C2的二元归结式(二元消解式)，C1和C2称作归结式的亲本子句，L1和L2称作消解文字。2012-5-813例设C1=P(x)∨Q(x)，C2=P(a)∨R(y)，求C1,C2的归结式。解：取L1=P(x)，L2=P(a)，则L1与L2的最一般合一者=｛a/x｝，于是，(C1-｛L1｝)∪(C2-｛L2｝)=(｛P(a),Q(a)｝-｛P(a)｝)∨(｛P(a),R(y)｝-｛P(a)｝)=Q(a)∨R(y)Q(a)∨R(y)是C1和C2的二元归结式。例设C1=P(x,y)∨Q(a)，C2=Q(x)∨R(y