人工智能自动推理(第3部分-归结原理及其应用)

3.8.1命题逻辑中的归结法Resolutionmethodinpropositionallogic设有命题逻辑描述的命题F1，F2,…,Fn和G,要求来证明在F1∧F2∧…∧Fn成立的条件下有G成立,或说F1∧F2∧…∧FnG是定理(重言式)，这就是我们的问题。如何建立推理规则，来证明这个定理便是我们的任务。很显然F1∧F2∧…∧FnG是重言式等价于F1∧F2∧…∧Fn∧～B是矛盾(永假)式。归结推理方法就是从F1∧F2∧…∧Fn∧～B出发，使用归结推理规则来寻找矛盾，最后证明定理F1∧F2∧…∧FnG的成立。这种方法可称作反演推理方法。子句与子句集Clauseandclauseset为使用归结方法，首先要把F1∧F2∧…∧Fn∧～G化成一种称作子句形的标准形式。一般地，归结推理规则所应用的对象是命题或谓词公式的一种特殊的形式，称为子句(Clause)一个子句就是一组文字的析取，一个文字或是一个原子(这时也称为正文字)，或者是一个原子的否定(这时也称为负文字)，如都是文字，是子句。~PQR、、~PQR我们知道：对任意公式，都有与之等值的合取范式，即对任意公式都有形如的公式与之等价，其中每个都是文字的析取式，就是一个子句。可以使用各种等价式将任意一个公式G转化为一个合取范式。例如，可以把公式转换为如下的合取范式:一个子句的合取范式(CNF形式)常常表示为一个子句的集合，即：称为对应公式的子句集，其中每个元素都是一个子句。把公式表示为子句集只是为了说明上的方便。{~,~~}SPRQRPG1...(1)nGGniG~()()PQRP(~)(~~)PRQRP归结式Resolvent命题逻辑的归结规则可以陈述如下。设有两个子句:(其中、是子句,是文字),从中消去互补对(即和),所得的新子句:，便称作子句，的归结式，原子称为被归结的原子。这个过程称为归结。没有互补对的两个子句没有归结式。因此归结推理规则指的是对两个子句做归结，即求归结式。上述归结规则是一种合理的推理规则，这可从下述定理中看出。''1122,~CPCCPC1C2CPP~P''1212(,)RCCCC1C2CP定理3.2子句和的归结式是和的逻辑推论。证明：设有其中和都是文字的析取式。''1122,~CPCCPC''1212(,)RCCCC1C1C2C2C'1C'2C假定和根据某种解释为真。若按解释为假，则必不是单元子句(即单个文字),否则按解释为假。因此，按必为真，即归结式按为真。若按I解释为真，则按I为假，此时必不是单元子句，并且必按为真，所以按I为真。由此得出，是和的逻辑推论。定理得证2C2C2C1C1C1CPPIIIII1C''1212(,)RCCCC~PI'2C1C12(,)RCC''1212(,)RCCCCProof:例3.3计算下述子句的归结式：（1）子句中的文字和子句中的文字是互补的。由和中分别删除和,并且构造两个子句的其余部分和的析取式，得出归结式为。这两个被归结的子句可以写成：,根据假言三段论，可以推出,它等价于。因此可以知道假言三段论是归结的一个特例。12:,:~CPRCPQ1C2CP~P1C2CP~PRQRQ~,RPPQ~RQRQ（2）和的归结式为。因为可以写作,所以可以知道假言推理也是归结的一个特例。（3）和存在两个归结式，一个是另一个是:。在这个例子中，只能是在上或上进行归结，不能两者同时进行归结，也就是说不是归结式。12:~,:CPQCP12:~,:~~CPQRCQR1C1C1C2C2CQQPQ~~PRR~~PQQ~PR（4）中的任何文字都不能与中的文字构成互补对，所以和不存在归结式。（5）和是互补的，将它们分别由和中删除，再构造和其余部分的析取式，得出的归结式是空子句(Nullclause)，用□表示。这说明由于和的互补性，它们不能同时成立。所以空子句的出现代表出现了矛盾。1C1C1C1C2C2C2C2CQQ12:~,:~CPQCPR12:,:~CQCQ~Q~Q归结推理过程Resolutionreasoningprocedure从子句集S出发，仅只对S的子句间使用归结推理规则，并将所得归结式仍放入S中，进而再对新子句集使用归结推理规则，重复这些步骤直到得到空子句□，便说明S是不可满足的，从而与S对应的定理F1∧F2∧…∧FnG是成立的。因为归结推理规则是正确的推理规则，归结式是原两子句的逻辑推论，于是归结过程出现空子句□，说明S中必有矛盾。例3.4证明先将化成合取范式，得建立子句集对S做归结(1)(2)(3)(4)（1）（2）归结(5)□（3）（4）归结证毕。()~~PQQP()~~(~)PQQP(~)~PQQP{~,~,}SPQQP~PQ~QP~P3.8.2谓词逻辑中的归结法Resolutionmethodinpredicatelogic和命题逻辑一样，在谓词逻辑中也具有归结推理规则和归结反演过程。只是由于谓词逻辑中存在量词、个体变元等问题，使得谓词逻辑中的归结问题比命题逻辑中的归结问题复杂很多。下面就来介绍谓词逻辑中的归结法。子句型Clauseform归结证明过程是一种反驳程序，即：不是证明一个公式是有效的(valid)，而是证明公式之非是不可满足的(unsatisfiable)。这完全是为了方便，并且不失一般性。我们知道，归结推理规则所应用的对象是命题或谓词合式公式的一种特殊的形式，称为子句。因此在进行归结之前需要把合式公式化为子句式。在第3.1节中已经介绍了如何把一个公式化成前束标准型,由于M中不含量词总可以把它变换成合取范式。无论是前束标准型还是合取范式都是与原来的合式公式等值的。11()...()nnQxQxMSkolem标准化过程111()...()(,...,)nnnQxQxMxxStep1:化成前束范式:Step2:使用下述方法可以消去前缀中存在的所有量词令是中出现的存在量词.rQ11()...()nnQxQx(1)rnCase1:若在之前不出现全称量词，则作置换:{c/xr}，c是一个与M中出现的所有常量都不相同的新常量c，用c代替M中出现的所有xr，并且由前缀中删去。rQrQCase2:若在之前出现全称量词，则选择一个与M中出现的任一函数符号都不相同的新m元函数符号f，用代替M中的所有xr，并且由前缀中删去。rQ1,...,ssmQQ1(,...,)ssmfxxrQ按上述方法删去前缀中的所有存在量词之后得出的公式称为合式公式的Skolem标准型。替代存在量化变量的常量c(视为0元函数)和函数f称为Skolem函数。(,,,,,)xyzuvwPxyzuvwxu例3.5化公式为Skolem标准型。在公式中，的前面没有全称量词，在的前面有全称量词和,在的前面有全称量词，和。所以，在中，用常数a代替x,用二元函数f(y,z)代替u,用三元函数g(y,z,v)代替w,去掉前缀中的所有存在量词之后得出Skolem标准型：(y)(z)(v)P(a,y,z,f(y,z),v,g(y,z,v))()y()z()w()y()z()v(,,,,,)PxyzuvwSkolem标准型的一个重要性质如下。定理3.3令为公式的Skolem标准型，则是不可满足的，当且仅当是不可满足的。证明不妨假设已经是前束范式，即设为前缀中的第一个存在量词。令其中，是对应的Skolem函数。我们希望证明是不可满足的，当且仅当是不可满足的。SGGSG111()...()(,...,)nnnGQxQxMxx()rrQx1111111111()...()()()(,...,,(,...,),,...,)rrrnnrrrnGxxQxQxMxxfxxxx11(,...,)rfxxrxG1G设是不可满足的。若是可满足的，则存在某定义域D上的解释I使按I为真。即对任意按I为真，所以，对任意，都存在元素使按I为真，那么G按I为真。这与G是不可满足的假设相矛盾。所以必是不可满足的。G1G1G11,...,rxDxD1111111()...()(,...,,(,...,),,...,)rrnnrrrnQxQxMxxfxxxx11,...,rxDxD11(,...,)rrfxxxD11111()...()(,...,,,,...,)rrnnrrrnQxQxMxxxxx1G另一方面，设是不可满足的。若G是可满足的，则存在某定义域D上的解释I使按I为真。即对任意,存在元素使按I为真。扩充解释I，使得包括对任意把映射成的函数f，即扩充后的解释用I1表示。显然，对任意按I1为真。即，这与是不可满足的假设相矛盾。所以必是不可满足的。1GG11,...,rxDxDrxD11111()...()(,...,,,,...,)rrnnrrrnQxQxMxxxxx11,...,rxDxD11(,...,)rxxrxD11(,...,)rrfxxx11,...,rxDxD1111111()...()(,...,,(,...,),,...,)rrnnrrrnQxQxMxxfxxxx11|GIT1GG假设中有m个存在量词。令，设是在中用Skolem函数代替其中第一个存在量词所对应的所有变量，并且去掉第一个存在量词而得出的公式,(k=1,…,m),显然。与上面的证明相似，可以证明是不可满足的，当且仅当是不可满足的(k=1,…,m)。所以可以断定，是不可满足的，当且仅当是不可满足的。G0GGkG1kGmSG1kGkGGS例3.6的SKOLEM标准形与并不是等值的。考虑论域为D={1,2},这时=取:P(1)=FP(2)=T有=T而的Skolem标准形：设定a为1,这时=F，与不等值。直观地说,是的一个具体的例化，考虑到存在量词有“或”的含义，然不能保证真必有真。为真,只要在论域D中能找到一个个体使为真。而=P(a)是从论域中选定一个个体a，这样不能保证P(a)为真。()()GxPxG()()GxPx(1)(2)PPGI|GIGG1()GPa1GG1GG1G()()xPx0x0()PxG1G显然下不能决定的真值，因为尚需对Skolem函数f(1),f(2)做设定。或说不是公式的解释。若设定f(1)=2，f(2)=2方构成的一个解释例3.7考虑与的逻辑关系。仍在论域D={1,2}上讨论。便有取：有=T()()(,)GxyPxy1()(,())GxPxfxG1G((1,1)(1,2))((2,1)(2,2))GPPPPGI(1,1),(1,2),(2,1),(2,2)PTPFPFPT|GIG1(1,(1))(2,(2))GPfPfGI1GGI1G1G1{(1)2,(2)2}GGIIff然而=F。同例3.6一样，只是的一个示例，不能保证真必真。然而反过来却有=T=T也即一般情形下有总之，与并不等值，但在不可满足的意义下是一致的。而且是的逻辑推论，反过来不成立。11|GIG1GGG1G11|GIG|GIG1GGSGSGSG注意:一个公式可以有几种形式的Skolem标准型。为简单起见，在变换公式时Skolem标准型时应该用尽量简单的Skolem函数代替G中存在量化的变量。即，应该使用变元个数量最少的Skolem函数。这意味着，在化为前束标准型时，应该使存在量词尽量向左移。例3.8将合式公式化为子句形。解：（1）消去蕴涵符号：这可以利用等价式：得到：（2）减少否定符号的辖域，把“”移到紧靠谓词的位置上：这可以利用下述等价式：[()[[()((,))]~[(,)()]]]xPxyPyPfxyyQxyPy~PQPQ[~()[[~()((,))]~[~(,)()]]]xPxyPyPfxyyQxyPy~