第四章自动推理(ppt).ppt

自动推理,自动推理的理论和技术是专家系统、程序推导、程序正确性证明、智能机器人等研究领域的重要基础。自动推理早期的工作主要集中在机器定理证明。1930年herbrand为定理证明建立了一种重要方法，他的方法奠定了机械定理证明的基础。机械定理证明的主要突破是1965年由j.a.robinson做出的，他建立了所谓归结原理，使机械定理证明达到了应用阶段。,agenda,引言命题逻辑中的归结原理谓词逻辑中的归结原理非单调推理,引言（1）,从一个或几个已知的判断(前提)逻辑地推论出一个新的判断(结论)的思维形式称为推理,这是事物的客观联系在意识中的反映。自动推理早期的工作主要集中在机器定理证明。机械定理证明的中心问题是寻找判定公式是否是有效的（或是不一致的）通用程序。若按推理过程中推出的结论是否单调地增加，或者说推出的结论是否越来越接近最终目标来划分，推理可以分为单调推理和非单调推理。,引言（2）,所谓单调推理是指在推理过程中随着推理的向前推进以及新知识的加入，推出的结论呈单调增加的趋势，并且越来越接近最终目标，在推理过程中不会出现反复的情况，即不会由于新知识的加入否定了前面推出的结论，从而使推理又退回到前面的某一步。所谓非单调推理是指在推理过程中由于新知识的加入，不仅没有加强已推出的结论，反而要否定它，使得推理退回到前面的某一步，重新开始。非单调推理是在知识不完全的的情况下发生的。,引言（3）,在现实世界中存在大量不确定问题。不确定性来自人类的主观认识与客观实际之间存在差异。事物发生的随机性,人类知识的不完全、不可靠、不精确和不一致,自然语言中存在的模糊性和歧义性都反映了这种差异,都会带来不确定性。针对不同的不确定性的起因,人们提出了不同的理论和推理方法。在下章中，我们将对不确定性推理进行讨论。,引言（4）,证明的基本思想是：设f1、fn、g为公式，g为f1、fn的逻辑推论，当且仅当公式（f1fn）g）是有效的也可以采用反证法的思想：设f1、fn、g为公式，g为f1、fn的逻辑推论，当且仅当公式（f1fng）是不可满足的归结法的本质上就是一种反证法，它是在归结推理规则的基础上实现的：为了证明一个命题p恒真，它证明其反命题p恒假，即不存在使得p为真的解释,agenda,引言命题逻辑中的归结原理谓词逻辑中的归结原理非单调推理,命题逻辑中的归结原理,子句和子句形归结归结反演合理性和完备性归结反演的搜索策略,子句和子句形（1）,文字是原子或其否定子句是文字的析取完备连接符集合：合取范式（cnf）（l11l1n1)(lm1lmnm)析取范式（dnf）（l11l1n1)(lm1lmnm)定理：对任意公式，都有与之等值的合取范式和析取范式转换方法：一般方法真值表方法,子句和子句形（2）,一般方法eliminateimplicationsignsbyusingtheequivalentformusingreducethescopesofsignsbyusingdemorganslawandbyeliminatingdoublesignsconverttocnfbyusingtheassociativeanddistributivelaws.,resolution,对任意三个文字p、q和rpr,qrpq或者：forc1=pc1,c2=pc2pc1,pc2c1c2归结式：r(c1,c2)=c1c2证明：,resolutionrefutations（1）,定理证明的任务:由前提a1a2.an推出结论b即证明:a1a2.anb永真转化为证明:a1a2.anb为永假式归结推理就是:从a1a2.anb出发,使用归结推理规则来找出矛盾,最后证明定理a1a2.anb的成立,resolutionrefutations（2）,归结方法是一种机械化的,可在计算机上加以实现的推理方法可认为是一种反向推理形式提供了一种自动定理证明的方法,resolutionrefutations（3）,一般过程:建立子句集s从子句集s出发,仅对s的子句间使用归结推理规则如果得出空子句,则结束;否则转下一步将所得归结式仍放入s中对新的子句集使用归结推理规则转(3)空子句不含有文字,它不能被任何解释满足,所以空子句是永假的,不可满足的归结过程出现空子句,说明出现互补子句对,说明s中有矛盾,因此s是不可满足的.,resolutionrefutations（4）,例子:证明(pq)qp首先建立子句集:(pq)q(p)(pq)qps=pq,q,p对s作归结:(1)pq(2)q(3)p(4)p(1)(2)归结(5)(3)(4)归结,soundnessandcompleteness,归结原理是合理的归结原理是完备的,resolutionrefutationsearchstrategies,有序策略（orderstrategies）refinementstrategies支持集（setofsupport）:每次归结时，参与归结的子句中至少应有一个是由目标公式的否定所得到的子句，或者是它们的后裔该策略是完备的线性输入（linearinput）：参与归结的两个子句中至少有一个是初始子句集中的子句该策略是不完备的祖先过滤（ancestryfiltering）：参与归结的两个子句中至少有一个是初始子句集中的句子，或者是另一个子句的祖先该策略是完备的,agenda,引言命题逻辑中的归结原理谓词逻辑中的归结原理非单调推理,谓词逻辑归结方法,子句形归结原理归结的完备性,子句形-skolem标准型,前束范式(q1x1)(qnxn)m(x1,xn)前束形=(前缀)母式量词串无量词公式定理：任何公式g都等价于一个前束范式skolem函数：存在量词不出现在全称量词的辖域内,此时只要用一个新的个体常量(称为skolem常量)替换受该存在量词约束的变元就可消去存在量词存在量词位于一个或多个全称量词的辖域内.此时需要skolem函数,该函数的变元就是由那些全称量词所约束的全称量词量化的变量.skolem函数所使用的函数符号必须是新的.,子句形-skolem标准型,skolem标准型：没有存在量词的公式。设g是一阶逻辑中的公式，将其化为skolem标准型，母式m给出的子句集s称为公式g的子句集,子句形化子句集-1,谓词公式化为子句形的步骤xp(x)yp(y)p(f(x,y)yq(x,y)p(y)(1)消去蕴含符号:pqpqxp(x)yp(y)p(f(x,y)yq(x,y)p(y)(2)减少否定符号的辖域,把“”移到紧靠谓词的位置上(p)p(pq)pq(pq)pq(x)p(x)p(x)p(x)pxp(x)yp(y)p(f(x,y)yq(x,y)p(y),子句形化子句集-2,(3)变量标准化:重新命名变元名,使不同量词约束的变元有不同的名字.xp(x)yp(y)p(f(x,y)wq(x,w)p(w)(4)消去存在量词:xp(x)yp(y)p(f(x,y)q(x,g(x)p(g(x),子句形化子句集-3,(5)化为前束形:把所有的全称量词移到公式的左边,并使每个量词的辖域包含这个量词后面公式的整个部分.即得前束形上例变为:xyp(x)p(y)p(f(x,y)q(x,g(x)p(g(x)(6)把母式化为合取范式:上例变为:xyp(x)p(y)p(f(x,y)p(x)q(x,g(x)p(x)p(g(x),子句形化子句集-4,(7)消去全称量词:p(x)p(y)p(f(x,y)p(x)q(x,g(x)p(x)p(g(x)(8)消去连结词符号p(x)p(y)p(f(x,y)p(x)q(x,g(x)p(x)p(g(x)(9)更换变量名称:对变元更名,使不同子句中的变元不同名.p(x1)p(y)p(f(x1,y)p(x2)q(x2,g(x2)p(x3)p(g(x3),子句形化子句集-6,一个子句内的文字可含有变量,但这些变量总是被理解为全称量词量化的变量g与其子句集s并不等值.但是在不可满足的意义下两者是等价的.而且g是s的逻辑推论,sg.反过来不成立,谓词逻辑的子句形-定理,定理:若g是给定的公式,而相应的子句集为s,则g是不可满足的当且仅当s是不可满足的推论：设g=g1gn,si是gi的skolem标准型，令s=sisn，则，g是不可满足的当且仅当s是不可满足的。,示例-1,例1:证明梯形的对角线与上下底构成的内错角相等设给定梯形的顶点依次为:a,b,c,d.t(x,y,u,v):表示以xy为上底,uv为下底的梯形p(x,y,u,v):表示xy平行于uve(x,y,z,u,v,w):表示xyz=uvw问题的逻辑描述和相应的子句集为:a1:(x)(y)(u)(v)(t(x,y,u,v)p(x,y,u,v)sa1:t(x,y,u,v)p(x,y,u,v)a2:(x)(y)(u)(v)(p(x,y,u,v)e(x,y,v,u,v,y)sa2:p(x,y,u,v)e(x,y,v,u,v,y),示例-1(续）,a3:t(a,b,c,d)(已知)sa3:t(a,b,c,d)b:e(a,b,d,c,d,b)(要证的结论)sb:e(a,b,d,c,d,b)因此:s=sa1sa2sa3sb,示例-2,例2:对所有的x,y,z来说,如果y是x父亲,z是y的父亲,则z是x的祖父.又知道每个人都有父亲,试问对某个人来说,谁是他的祖父?引入谓词:p(x,y):表示x是y的父亲q(x,y):表示x是y的祖父a1:(x)(y)(z)(p(x,y)p(y,z)q(x,z)sa1:p(x,y)p(y,z)q(x,z)a2:(y)(x)p(x,y)sa2:p(f(y),y),示例-2（续）,b:(x)(y)q(x,y)(要证的结论)sb:q(x,y)ans(x)其中ans(x)是人为增加的,在推理过程中,ans(x)变量x同q(x,y)中的x作同样的变换,当推理结束的时候,ans(x)中的变量x便给出了问题的解答因此:s=sa1sa2sb,谓词逻辑中的归结原理,置换与合一归结式归结反演,置换(substitution)（1）,例：c1：p(x)q(x)c2：p(f(x)r(x)没有互补对;例：c1：p(y)q(y)y/xc1：p(f(x)q(f(x)f(x)/yc3：r(x)q(f(x),置换(2）,置换和合一是为了处理谓词逻辑中子句之间的模式匹配而引进.定义:置换是形如t1/v1,t2/v2,tn/vn的一个有限集.其中vi是变量,而ti是不同于vi的项(常量,变量,函数),且vivj(ij),i,j=1,n例子：a/x,w/y,f(s)/z,g(x)/x是置换;x/x,y/f(x)不是置换;,置换-（3）,定义：不含任何元素的置换称为空置换，记为定义:设=t1/v1,t2/v2,tn/vn是一个置换，e是一个表达式。将e中出现的每一个变量符号vi（1in）,都用项ti置换，这样得到的表达式记为e，称e为e的例。,置换-（4）,例子：e=p(x,y,z),=a/x,f(b)/y,c/ze=p(a,f(b),c)e=p(x,g(y),h(x,z),=a/x,f(b)/y,g(w)/ze=p(a,g(f(b),h(a,g(w)e=p(x,y,z),=y/x,z/ye=p(y,z,z).ep(z,z,z).(同时),置换的复合（乘积）（1）,例子:e=p(x,y,z)=a/x,f(z)/y,w/ze=p(a,f(z),w)=t/z,g(b)/we=p(a,f(t),g(b)=a/x,f(t)/y,g(b)/z,置换的复合（乘积）（2）,定义：设=t1/x1,t2/x2,tn/xn和=u1/y1,u2/y2,um/ym是两个置换,也是一个置换,可定义为:先作置换:t1/x1,t2/x2,tn/xn,u1/y1,u2/y2,um/ym若:yi(x1,x2,xn)则删除ui/yi若:ti=xi,则删除ti=xi所得的置换称为和的复合或乘积,记为,置换的复合（乘积）-（3）,定理：设和是两个置换,e是表达式，则e()=(e)设,是三个置换,则有:置换满足结合率:()=()置换的交换率不成立=,置换的复合（乘积）-（4）,=a/x,=b/x=a/x=b/x,合一（unification）（1）,定义:设有公式集e=e1,.,en和置换,使得:e1=e2=en则称e1,.,en是可合一的,并且称为一合一置换.也称为e1,en的合一子(unifier).定义：如果对e1,en存在这样的合一子,则称集合e1,en是可合一的.,合一（unification）（2）,例1:e=p(a,y),p(x,f(b),=a/x,f(b)/y.e=p(a,b),p(x,f(b)合一子不一定唯一e=p(a,y),p(x,f(b)1=a/x,f(b)/y(唯一)e=p(x,y),p(x,f(b)1=a/x,f(b)/y(不唯一)2=b/x,f(b)/y,最一般合一（1）,定义:设是公式集e的一个合一,如果对于任一个合一,都存在置换使得:=,则称是公式集e的最一般合一置换,记为mgu(mostgeneralunifier),最一般合一（2）,例子:e=p(x,y),p(x,f(b)1=a/x,f(b)/y2=b/x,f(b)/y=f(b)/y1=a/x2=b/x,差异集合,设w是非空表达式集合，w的差异集合d定义如下：首先找出w的所有表达式中不是都相同的第一个符号，然后从w的每个表达式中抽出占有这个符号位置的子表达式，所有这些子表达式组成的集合就是w的差异集合d。若d中无变量符号，则w是不可合一的若d中只有一个元素，则w是不可合一的若d中的变量符号x和t，且x出现在t中，则w是不可合一的例子:w=p(x,f(y,z),z，w),p(x,a),p(x,g(z),z,b)d=f(y,z),a,g(z),合一算法（1）,(1)令k=0,w0=w(w=e1,e2),0=(2)如果wk已经合一,则算法停止,k=mgu否则，求出wk的差异集dk(3)如果dk中存在元素xk,tk,且xk不在tk中出现,则转(4)；否则不可合一，停止(4)令k+1=ktk/xkwk+1=wktk/xk=wk+1(5)k=k+1然后转(2),合一算法（2）,换名:p(f(x),x),p(x,a);如果不换名：d=f(x),x.换名:p(f(y),y),p(x,a);mgu:f(a)/x,a/y,合一算法（3）,求w=p(a,x,f(g(y),p(z,f(z),f(u)的mgu.d0=a,z.1=a/z=a/z.w1=w01=p(a,x,f(g(y),p(a,f(a),f(u)d1=x,f(a).2=1f(a)/x=a/z,f(a)/x.w2=w12=p(a,f(a),f(g(y),p(a,f(a),f(u)d2=g(y),u.3=2g(y)/u=a/z,f(a)/x,g(y)/uw3=w23=p(a,f(a),f(g(y)3是mgu.,合一算法（4）,求w=q(f(a),g(x),q(y,y)的mgu.d0=f(a),y.1=f(a)/y=f(a)/y.w1=w01=q(f(a),g(x),q(f(a),f(a)d1=g(x),f(a).不可合一,没有mgu.,合一算法（5）,求w=p(f(y),y),p(x,a)的mgu.d0=f(y),x.1=f(y)/x=f(y)/x.w1=w01=p(f(y),y),p(f(y),a)d1=y,a.2=1a/y=f(y)/xa/y=f(a)/x,a/y.w2=w12=p(f(a),a)2是mgu.,合一算法（6）,性质：若w是关于表达式的有限非空可合一集合，则合一算法将在第（2）步结束，并且最后的k是w的mgu。若一组表达式e1,en是可合一的，则它们的mgu除了相差一个改名外，是唯一确定。,归结式,定义:设c1和c2是两个无公共变量的子句,l1和l2分别是c1和c2的文字,如果l1和l2有mgu:,则:(c1-l1)(c2-l2)称为c1和c2的一个二元归结式,而l1l2称为被归结的文字若r(c1,c2)是c1,c2的二元归结式,则:c1c2=r(c1,c2),归结式-例子（1）,c1:p(x)q(x)c2:p(a)r(x)重命名c2:p(a)r(y)l1=p(x),l2=p(a)l1与l2有mgu=a/x(c1l1)(c2l2)=(p(a),q(a)p(a)(p(a),r(y)p(a)=q(a)r(y)=q(a),r(y)q(a)r(y)是c1与c2的二元归结式.,归结式-例子（2）,c1=p(x)q(x)c2=p(g(y)q(b)r(x)1=g(y)/x:r(c1,c2)=q(g(y)q(b)r(x)2=b/x:r(c1,c2)=p(g(y)p(b)r(x),归结式因子,定义：如果一个子句c的几个文字有mgu,则c称为子句c的因子例子设c=p(x)p(f(y)q(x)假设=f(y)/x,则:c=p(f(y)q(f(y),归结式,定义:设c1和c2是无公共变量的子句,其归结式是下列二元归结式之一:(1)c1和c2的二元归结式(2)c1的因子和c2的二元归结式(3)c1和c2的因子的二元归结式(4)c1的因子和c2的因子的二元归结式该归结式仍记为r(c1,c2),归结式-2,例:c1=p(x)p(f(y)q(g(y)c2=p(f(g(x)q(b)c1的因子为:=f(y)/x,c1=p(f(y)q(g(y)则:r(c1,c2)=q(g(g(x)q(b),归结反演,设e为已知前提的公式集,q为目标公式(或结论),用归结反演证明q为真的步骤为:(1)否定q得到q(2)把q加入到公式集e中,得到e,q(3)把公式集e,q化为子句集s(4)应用归结原理对子句集s中的子句进行归结,并把每次归结所得的归结式并入s中.如此反复进行,若出现空子句,则停止归结,此时就证明了q为真.,归结反演示例一,已知：求证：,归结反演示例二,给定下面一段话：tony、mike和john都是alpineclub的会员。每个会员或者是一个滑雪爱好者，或者是一个登山爱好者，或者都是。没有一个登山爱好者喜欢下雨，所有的滑雪爱好者都喜欢雪。tony喜欢的所有东西mike都不喜欢，tony不喜欢的所有东西mike都喜欢。tony喜欢雨和雪。用谓词演算表达上述信息。把问题“谁是该俱乐部的会员，他是一个登山爱好者，但不是滑雪爱好者”表达为一个谓词表达式，用归结反驳提取答案,归结的完备性,问题的提出：若定理成立，是否使用归结方法必能得到证明？或者说：使用归结方法推出的定理的个数和所有成立的定理的个数是否一样多？,herbrand定理,由来为了评定子句集的不可满足性,就需要对子句集中的子句进行评定.一般情况下,要评定一个子句的不可满足性,需要对个体域上的一切解释逐个地进行评定.但是由于个体变量论域的任意性,以及解释个数的无限性,因此评定子句集的不可满足性是很困难的.herbrand域就是一个特殊的域,只要在这个论域上公式不可满足,则该公式就在任一论域上也不可满足,herbrand定理-h域,定义:设s为子句集,则按下述方法构造的域h称为h域:(1)令h0是s中所有的个体常量的集合,若s中不包含个体常量,则任取常量ad,而规定h0=a(2)令hi+1=hi所有形如f(t1,tn)的元素其中:f(t1,tn)是出现于s中的任一函数,而t1,tn是hi中的元素.i=1,2,.h域是直接依赖于s的最多只有可数个元素,herbrand定理-h域,例一:s=p(a),p(x)p(f(x)根据定义有:h0=ah1=af(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),.例二:s=p(x),q(y)r(z)h0=h1=h=a,herbrand定理-h域,例三：s=p(f(x)，a，g(y)，b)h0=a，bh1=a，b，f(a)，g(a)，f(b)，g(b)h2=a，b，f(a)，g(a)，f(b)，g(b)，f(f(a)，f(g(a)，f(f(b)，f(g(b)，g(f(a)，g(g(a)，g(f(b)，g(g(b).,herbrand定理-h域,基础(ground)/基没有变量的项称为基础项(groundterm).f(a,b)没有变量的原子称为基础原子(groundatom).p(a,f(b)没有变量的文字称为基础文字(groundliteral).p(a,f(b),p(a,f(b)没有变量的子句称为基础子句(groundclause).p(b,f(b)q(f(f(b),herbrand定理-h域,原子集:子句中所有基原子构成的集合称为原子集.令s是一个子句集合,形如p(t1,.,tn)的基础原子集合,称为s的原子集.记为a.其中,p(t1,.,tn)是出现在s中的任一谓词符号,而t1,.,tn是s的h域的任意元素。,herbrand定理-h域,s=p(z),p(x)q(y)h=aa=p(a),q(a)s=p(a),p(x)p(f(x)h=a,f(a),f(f(a),.a=p(a),p(f(a),p(f(f(a),.s=p(f(x),a,g(y),b)h=a,b,f(a),g(a),f(b),g(b),a=p(a,a,a,a),p(a,a,a,b),p(a,a,b,b),.,herbrand定理-h域,定义(基础实例)当s中的某子句c中所有变量符号均以s的h域的元素代入时，所得的基子句c称作c的一个基础实例(基例）例s=p(x),q(f(y)r(y),z(f(y)h=a,f(a),f(f(a),.p(a),p(f(a)都称作子句c=p(x)的基例。同样,q(f(a)r(a),q(f(f(a)r(f(a)都是q(f(y)r(y)的基例。q(a)r(a)不是q(f(y)r(y)的基例。对于任一bd,子句p(b),q(f(b)r(b)都叫基子句。,herbrand定理-h的解释,起因由子句集s建立h域、原子集a;一般论域d上对s的解释ih域上的解释i*;s在d上为真s在h上为真;s在d上不可满足s在h上不可满足;,herbrand定理-h的解释,h解释的表示令a=a1,an,是s的原子集,一个h解释可被表示为:i=m1,mn,其中mj或者是aj或者是aj.如果mj是aj,则aj为真,否则,aj为假.,herbrand定理-h的解释,定义:子句集s在h域上的一个解释i*满足下列条件:(1)在解释i*下,常量映射到自身(2)s中的任一n元函数是hnh的映射.即假设h1,h2,hnh,则f(h1,h2,hn)h(3)s中的任一个n元谓词是hnt,f的映射.,herbrand定理-h的解释,例子:s=p(x)q(x),r(f(y)h=a,f(a),f(f(a),.a=p(a),q(a),r(a),p(f(a),q(f(a),r(f(a),s的h解释,如:i*1=p(a),q(a),r(a),p(f(a),q(f(a),r(f(a),i*2=p(a),q(a),r(a),p(f(a),q(f(a),r(f(a),i*3=p(a),q(a),r(a),p(f(a),q(f(a),r(f(a),则有:s|i*1=t,s|i*2=f,s|i*3=f,herbrand定理-h的解释,由s在d域的解释i如何确定相应的s在h域的解释i*:(1)若s中有常量符号,任一ah0,在i下a取值为a0,就规定aa0(2)若s中无常量符号,h0=a,就规定aa0,a0是d的任一元素(3)若f(h1,h2,hn)是s中的任一函数符号,任取(h1,h2,hn)hni.当在i下(h1,h2,hn)取值为(h01,h02,h0n),且在i下对应值为f(h01,h02,h0n)(为d中的元素),就规定:f(h1,h2,hn)f(h01,h02,h0n)则i*是如下的h解释：vi*(p(h1,h2,hn)=vi(p(h01,h02,h0n),herbrand定理-h的解释,定理:设i是s的论域d上的解释,存在对应于i的h解释i*,使得如果s|i=t,则有s|i*=t定理:子句集s是不可满足的,当且仅当在所有的s的h解释下为假()设s是不可满足的.则在任一个论域上的任一解释使s为假;h是一个论域;()设s的所有的h解释使s为假.假设子句集s可满足.在某个论域上的某个解释i使s为真;i在h域上对应解释i*;根据引理，i*满足s.,herbrand定理-语义树,语义树是通过将s的所有解释展示在一棵树上,从几何上对s的不可满足性进行讨论example1g=pqrs=p,q,ra=p,q,r,herbrand定理-语义树,example2s=p(x)q(x),p(f(y),q(f(y)h=a,f(a),f(f(a),.a=p(a),q(a),p(f(a),q(f(a),.,herbrand定理-语义树,颠倒原子的顺序是可以的.例如q(a)为第一个顶点.如果原子集是无限的，则对应的语义树必定是无限的.从任一个叶节点向根节点看,代表s的一个解释.从任一个中间节点向根节点看,代表s的一个部分解释.,herbrand定理-语义树,语义树的特点:s的语义树是完全的,如果n表示叶节点,则i(n)包含了s的原子集中所有元素或者该元素的否定语义树每个直到叶节点的分枝都对应于s的一个解释.特别对有限树来说,i(n)就是s的一个解释如果节点n的i(n)使s的某一子句的某一集子句为假,而n的父辈节点不能评定这个事实,则称n为失败节点如果s的完全语义树的每个分枝上都有一个失败节点,就说该语义树为封闭语义树,herbrand定理-语义树,examples=p,qr,pq,pr,herbrand定理-语义树,封闭语义树：,p,p,q,q,r,r,herbrand定理-语义树,examples=p(x),p(x)q(f(x),q(f(a)a=p(a),q(a),p(f(a),q(f(a),p(a),q(f(a),p(a),q(f(a),herbrand定理-语义树,证明一个定理就是寻找一棵封闭语义树.s不可满足s在所有解释下为假s在所有h解释下为假;完备语义树包含所有h解释;每一枝是一个h解释;s在i下为假,则使某个基础实例为假;这个节点称为假节点,不用再扩展;所有枝上都有假节点,则为封闭语义树;,herbrand定理,herbrand定理(1):子句集s是不可满足的,当且仅当对应于s的完全语义树都是一棵有限封闭语义树,herbrand定理,herbrand定理(2):子句集s是不可满足的,当且仅当存在不可满足的s的有限基例集s例子:s=p(x),p(a)p(b),q(f(x)h=a,b,f(a),f(b),f(f(a),f(f(b)a=p(a),p(b),q(a),q(b),s=p(a),p(b),p(a)p(b),p(a),p(b),p(a),p(b),困难,生成基础实例集合是指数复杂性的例子:s=p(x,g(x),y,h(x,y),z,k(x,y,z),p(u,v,e(v),w,f(v,w),x)h0=ah1=a,g(a),h(a,a),k(a,a,a),e(a),f(a,a)基础实例集：s0=p(a,g(a),a,h(a,a),a,k(a,a,a),p(a,a,e(a),a,f(a,a),a)s1有6*6*6+6*6*6*6=1512个元素;h5有1064数量级的元素，s5有10256数量级的元素.,一些简化计算规则(1),重言式子句可删除规则s中的重言式子句，不会为s的不可满足提供任何信息，可以删除s=pp，q，rps的逻辑含义是（pp）q(rp)=q(rp)，从而删去重言式pp，不影响s的真值。s=q，rp,一些简化计算规则(2),单文字删除规则单文字:在s中存在只有一个文字的基础子句l.如s=l,lc1,lc2,c3,c4,其中c3,c4不含l和l.从s中删除含l的子句得到:s=lc2,c3,c4从s中删除文字l得到:s=c2,c3,c4若s为空,则s是可满足的若s不空,则s和s同时是不可满足的.,一些简化计算规则(3),纯文字删除规则定义:当文字l出现于s中,而l不出现于s中时,则称l为s的纯文字从s中删除含l的子句得s.如果s为空集,则s是可满足的如果s非空,则s与s同时是不可满足的例子:s=ab,ab,b,bs=b,b;,一些简化计算规则(4),分离规则若s=(la1)(lam)(lb1)(lbn)r其中r是不含l和l的文字集令s=a1,.,am,rs=(b1,bn,r则s不可满足当且仅当s和同时不可满足s,一些简化计算规则(5),s=pqr,pq,p,r,u对u使用纯文字:pqr,pq,p,r对p使用单文字:qr,q,r对q使用单文字:r,r对r使用单文字:s不可满足;s=pq,q,pqr对q使用单文字:p,pr对p使用单文字:r对r使用纯文字:s可满足；,归结和语义树“倒塌”过程,例：s=p,pq,pqa=p,q归结过程：(1)p(2)pq(3)pq(4)p(2)(3)(5)(1)(4),p,q,n11,n12,n21,n24,t,n0,p,q,n11,n12,n21,t*,n0,p,n11,t(1),归结的完备性,提升引理:c1、c2是无公共变量的子句，而c1、c2分别是c1、c2的例，r是c1、c2的归结式，则存在c1、c2的归结式r，使得r是r的例,归结的完备性,例子c1:p(x)q(f(x)c2:q(y)r(y)c1:p(a)q(f(a)a/xc2:q(f(a)r(f(a)f(a)/yc:p(a)r(f(a)c:p(x)r(f(x),归结的完备性,完备性定理：s是不可满足的当且仅当存在一个使用归结推理规则的从s到空子句的推理过程,效率的问题（1）,归结原理比herbrand定理有了明显的进步;盲目的归结会产生组合爆炸问题;不必要的归结式不必要的归结式;,效率的问题（2）,s=pq,pq,pq,pq盲目归结过程:s0=ssi=c1,c2的归结式|c1s0s1si-1,c2si-1具体过程:s0:(1)pq(2)pq(3)pq(4)pqs1:(5)q(1)(2)(6)p(1)(3)(7)qq(1)(4)(8)pp(1)(4).(12)qs2:(13)pq(1)(7)(14)pq(1)(8).(39)nil(5)(12),agenda,引言命题逻辑中的归结原理谓词逻辑中的归结原理非单调推理,非单调推理,什么是非单调推理主要的非单调逻辑封闭世界假设(cwa)限制理论缺省逻辑,什么是非单调推理(1),科学的发现过程是一个证伪的过程，人类知识的增长是一个非单调的过程传统的逻辑系统实际上作的是单调推理，加进系统的新知识（信念）必须与已有的知识（信念）相一致，不会引起矛盾。所以，随着运行时间的推移，系统内含的知识有增无减，这就是所谓的单调性。设fs为一个逻辑系统，如果对于fs的任意两个公式集合t和s，t是s的子集，则th(t)也是th(s)的子集(th(t)表示从t中推出的定理的集合=a|ta)这说明向一个公理理论中增加新的定理不会影响该理论已经有的定理，初始理论原来已经有的定理仍然是扩大了以后理论的定理。,什么是非单调推理(2),单调性的优点在于：（1）加入新命题时不需审查与系统原有知识的相容性，因为这些新命题只能是已有知识的逻辑推理结果，不可能引起矛盾。换言之，加入的新命题必定是永真的。（2）不需要记忆推导过程。因为推导的结论永远不会失败，不存在事后审查推导过程的需求问题。,什么是非单调推理(3),非单调性推理推理系统的定理集合并不随推理过程的进行而增大，新推出的定理很可能会否定、改变原来的一些定理。推理时所依据的知识具有不完全性逻辑系统是非单调的，如果存在公式集合t和s，如果ts，但th(t)th(s),什么是非单调推理(4),需要非单调推理的理由主要为：知识的不完全一个有限的信念集合仅仅是现实世界的近似描述，会有很多的例外-资格问题客观世界变化太快，一个不断变化的世界必须用变化的知识库加以描述框架问题非单调推理比单调推理难处理得多。因为当一个假设被发现错误而撤消时，一系列基于它的推理结果都要撤消。所以，设计非单调推理系统的一个关键问题在于防止系统花费过多的时间在这种处理上。,什么是非单调推理(5),非单调推理的研究有两条途径：对逻辑的扩展：这涉及非单调推理的形式化方面，称为非单调逻辑，它包括：语言方面的扩充（指增强其表达能力）和语义方面的扩充（指对真值的真假两种情况进行修正）；主要包括：基于最小化语义：主要有封闭世界假设、mccarthy的限制逻辑（circumscription）、konolige的忽略逻辑等基于定点定义：主要有缺省逻辑(default)和自认知逻辑(autoepistemic)等。对推理模式的扩展：这涉及非单调推理的过程化方面，称为非单调系统。这可以通过对矛盾的检测进行真值的修正来维护相容性，可称为真值维护系统。,什么是非单调推理(6),非单调推理的三个主要流派：mccarthy的限制理论：当且仅当没有事实证明s在更大的范围成立时，s只在指定的范围成立；reiter的缺省逻辑：“s在缺省的条件下成立”是指“当且仅当没有事实证明s不成立时s是成立的”。moore的自认知逻辑：“如果我知道s，并且我不知道有其他任何事实与s矛盾，则s是成立的”。,封闭世界假设(1),在非单调领域中的推理，我们必须给出下面的假设：封闭世界假设（closedworldassumption:cwa），或者增加新的事实，继续推理封闭世界假设是一种对由一组基本信念集合kb定义的理论t(kb)进行完备化的方法。我们说一个理论t(kb)是完备的，是说其包含（显式或隐含）了每一个基原子公式或该公式否定。cwa的基本思想是：如果无法证明p，则就认为它是否定的。即：如果从知识库中无法证明p或者p，则就向kb中增加p即假定知道所有有关世界的事情（世界是封闭的）,封闭世界假设(2),cwa是非单调的：cwa对理论的完备化是仅仅通过向基本信念集合kb中增加基原子公式的取反来实现的。一旦以后有新的基原子公式加进kb，则为完备t（kb）而生成的扩充集就必须收缩（删除该基原子公式的否定）。由于为完备t(kb)而生成的扩充集中的每个基原子公式的取反均是假设的暂时信念，记该扩充集为kbasm。对于一个基原子公式p，cwa可定义：pkbasm，当且仅当pt(kb)。经过由cwa方法完备的理论为cwa(kb),它扩大了t(kb)的推理能力,允许不能由kb导出的结论可以由kbkbasm导出.,封闭世界假设(3),cwa方法并不确保被完备的理论cwa(kb)是一致的，解决不一致性是非单调推理的重要议题，需要对cwa的完备性规则进行修改，以实现一致性。cwa(kb)是一致的，当且仅当对于每个可由kb推导出的子句p1p2pn，都至少存在一个pi可从kb推导出；其中pi均为正基文字。若kb是由一致的horn形子句组成时，则cwa(kb)必定一致,限制理论（1）,限制理论的核心思想是：如果一个句子叙述一个命题，那么它叙述的仅仅是这个命题，一点都不能扩张和延伸，任何多余的东西都要删除掉。这就是所谓的“occam剃刀原理”，mccarthy称为极小模型。限制理论最初是用于定义通常什么事物是成立的这可以在fol中定义一个”尽可能错”的特殊异常的谓词：ab然后通过最小化ab的扩展，最小化该异常性即除了那些已知为真的对象外，其他都为假,限制理论（2）,and_gate(x,in1,in2,out)zero(in1)ab(x)zero(out)block(x)ab(x)ontable(x)holds(f,t)ab(f,t+1)holds(f,t+1),限制理论（3）,限制有多种形式，如：平行限制（公式限制）论域限制谓词限制,平行限制,限制作为二阶公式：令p=q表示x(p(x)q(x)令pq表示x(p(x)q(x)令pq表示(pq)(p=q)令a(p)表示包含谓词p的句子a中p的限制circ(a;p)为：a(p)qa(q)qp直觉上看：p是使得a为真的最小的谓词之一。,论域限制,论域限制的含义是：只有那些存在的事物才是已知的，未知的事物都是不知道的。设为一阶公式，设个体域为x|p(x)，a为一个命题，(x)为带有自由