计算引论9推理与计算

,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,计算引论,第四章 推理与计算,4,推理与计算,预,备,知,识,Horn,逻辑程序,命题,Horn,逻辑中的自动推理,谓词,Horn,逻辑中的自动推理,4.1,预备知识,考虑到读者已学习数理逻辑，基本熟悉相关概念和知识，下面我们简单给出有关逻辑推理的基本概念。因为篇幅所限，为理解更加形象，概念定义形式未必采用数理逻辑中严格定义形式，准确概念请参见离散数学数理逻辑部分。,命题,在一阶逻辑中，命题陈述某个对象的性质，或是某些对象的关系。陈述的形式是作为,n,元函数的“谓词”与它的变量“项”。,例如命题“鸟会飞”表示为,canfly(bird)，,其中“,canfly”,是谓词，“,bird”,是项。,项,项,是指某个命题的“对象”或是“客体”。如下递归定义“项”,i,单个的常量和变量都是项。,ii,如果,f,是函数符,t,1,t,n,是项，那么,f(t,1,t,n,),也是项。,例如，,gcd,是表示最大公约数的函数符，,a+b,，,cd-2,是两个项，则,gcd(a+b,cd-2),也是项。,原子,若,P,是一个,n,元谓词符号，,t,1,t,n,是项,那么,P(t,1,t,n,),是,原子,例如，,father,是表示父子关系的二元谓词，则,father(John,Peter),是原子，表示,John,是,Peter,的父亲。这里,father(John,Peter),做为基本二元关系。,公式,如下递归定义“公式”,i,原子是公式,ii,若,P,Q,是公式，则,PQ,PQ,PQ,P,是公式,iii,若,P,是公式，,x,是,P,中的变量，则,(,x),P，(,x),P,是公式。,文字和子句,若,P,是原子，则,P,P,称为,文字,。,P,称为正文字，,P,称为负文字。,公式,P,称为,子句,，若,P,等值于,L,1,L,n,，,其中,L,1,L,n,是文字。,没有变量符号出现的项、原子、子句，,分别称为,基项、基原子、基子句,。,文字和子句（续）,例如，,gcd(45,b),是基项,father(John,Peter),是基原子,father(John,Peter),uncle(John,Peter),是基子句,Skolem,标准型,上面定义的公式，形式是很多样的。这就会给机器的形式化处理带来很大的麻烦。为了便于机器处理，需要把公式化成统一的标准形式，即,SKOLEM,标准型，进而建立子句集。,Skolem,标准型（续）,设,P,是公式，,P,等价于,x,1,x,n,G(x,1,.x,n,),，,并且,G,G,1,G,m,，,其中,G,1,G,m,都是子句，则称,G,的子句集,S=G,1,G,m,为公式,P,的,Skolem,标准型,。,Skolem,标准型（续）,对公式,P,的,SKOLEM,化的步骤如下：,（,1,）将,P,化为前束范式,（,Q,1,x,1,）,（,Q,n,x,n,）,H(x,1,.x,n,),其中,Q,1,Q,n,是存在量词或者全称量词，并将,H,化为合取范式的形式；,Skolem,标准型（续）,（,2,）用如下方法消去存在量词：,i),若,Q,i,是一个存在量词，并且它的左边没有全称量词，则用一个,H,中没有的常量符号代替,H,中所有的,x,i,，,之后消去（,Q,i,x,i,）,Skolem,标准型（续）,ii),若,Q,i,是一个存在量词，并且,Q,j1,Q,jk,是,Q,i,左边的全称量词，则取一个,H,中没有的函数,k,元符号,f,用,f(x,j1,x,jk,),代替,x,i,之后消去（,Q,i,x,i,）,。,Skolem,标准型（续）,公式,P,经过如上处理，可以化为,x,1,x,n,(G,1,G,m,),的形式,，,其中,G,1,G,m,都是子句。省略全称量词，再用“，”取代合取符号，便得到公式,P,的,Skolem,标准型,G,1,G,m,。,Skolem,标准型（续）,由以上可知，任意公式都有与之相对的子句集。子句集的形式是相对简单的。需要注意的是，一个公式与它的,Skolem,标准型未必等值，但在不可满足的意义上是一致的。,Horn,子句与,Horn,逻辑程序,如果在一个子句中最多含有一个正文字，那么该子句称为,Horn,子句,。,若一个子句集内的子句个数有限且都是,Horn,子句，那么该子句集称为一个,Horn,逻辑程序,。,替换,一个,替换,是形如,t,1,/x,1,t,n,/x,n,的一个有限集合。其中,x,i,（,i=1,n,）是两两不同的变量符号,t,i,是不同于,x,i,的项。,替换可以如下作用于一个表达式：给定替换,=t,1,/x,1,t,n,/x,n,和表达式,E,，,E,表示将,E,中出现的每一个,x,i,（,i=1,n,）都替换成,t,i,得到的新表达式。,替换（续）,给定两个替换,=t,1,/x,1,t,n,/x,n,=u,1,/y,1,u,m,/y,m,将集合,t,1,/x,1,t,n,/x,n,u,1,/y,1,u,m,/y,m,删去以下元素：,u,i,/y,i,，当,y,i,x,1,x,n,t,i,/x,i,，当,t,i,=x,i,得到的新替换表示为,，称为,和,的复合,。,合一替换,给定表达式,E,1,E,k,，,若存在替换,，使得,E,1,=E,k,，则称,是,E,1,E,k,的一个,合一替换,。,合一替换（续）,例,1,，设,E,1,=g(x,y),，,E,2,=g(a,f(z),。令,=a/x,f(h(u)/y,h(u)/z,，,则,E,1,=g(a,f(h(u),E,2,=g(a,f(h(u),因为,E,1,=E,2,，所以是,E,1,与,E,2,的合一,替换。,合一替换（续）,例,2,，设,E,1,与,E,2,同上，,=a/x,f(z)/y,，则,E,1,=g(a,f(z)=E,2,，所以也是,E,1,与,E,2,的合一替换。,显然比 简单，易证,=,，其中,=h(u)/z,4.2 Horn,逻辑程序,在知识工程中，知识要作为数据按一定格式存放在数据库中。,已知的知识表示方法有,产生式表示法,语义网络表示法,逻辑表示法,产生式表示法是一类很重要的方法，知识表示成,IF THEN,的形式。采用产生式方法，可以将规则与事实以统一的格式表示，即,Horn,子句。,4.2 Horn,逻辑程序,Horn,子句可以表示成如下形式：,规则体,规则头,其中规则体一般是,n,个原子的合取，,n=0,1,。规则头可以是单个原子，也可以是空。,4.2 Horn,逻辑程序,在,Horn,逻辑程序自动推理时用到如下概念：,规则：规则体非空且规则头非空的子句。例如，,father(z,y),father(y,x),grandfather(z,x),事实：规则体空且规则头非空的子句。例如，,father(John,Peter),。,目标：无规则头的子句，例如，,grandfather(Smith,Peter),，即要查询,Smith,是否是,Peter,的祖父？,4.2 Horn,逻辑程序,一个,Horn,逻辑程序是,Horn,子句的集合，也就是规则和事实的集合。因此，一个,Horn,逻辑程序相当于一个知识库。,知识库应当具有自动推理的能力。所谓推理，实际上是通过对一组子句按照一定的方式进行消解最终得到新的公式。,4.2 Horn,逻辑程序,自动推理的过程即给定目标子句，机器按照一定的顺序对逻辑程序中的子句进行消解，最后得到目标子句，或者得出目标不可满足的结论。,4.2 Horn,逻辑程序,因为,Horn,子句结构特殊，,Horn,逻辑程序上的消解过程简单。下面分别在命题,Horn,逻辑和谓词,Horn,逻辑情形下给出消解过程。,4.3,命题,Horn,逻辑中的自动推理,在命题,Horn,逻辑中，子句之间可以按照如下的方式消解。若有子句,S,1,：,A,1,A,n,S,2,：,B,1,B,m,A,i,则归结后的子句为,S,3,：,A,1,A,i-1,B,1,B,m,A,i+1,A,n,即利用规则,S,2,将原目标,S,1,转化为新目标,S,3.,4.3,命题,Horn,逻辑中的自动推理,基于上述消解方式，求证一个目标,S,：,A,1,A,n,需要逐一以,S,的体中的每一个原子,A,i,作为新的目标进行求证。,A,1,A,n,也称为,S,的子目标。,在以一个原子,A,i,为目标进行求证时，考察子句集内所有头部是,A,i,的子句，以此子句的体作为新的目标。,4.3,命题,Horn,逻辑中的自动推理,当某个关于,A,的子句体部的所有原子得到满足时，直接返回,A,是正确的，而不用再接着考察头是,A,的其他子句。,假如对于某个原子,A,，逻辑程序中所有头部是,A,的子句都无法满足，则得出,A,无法满足的结论,。,原子,A,的推理算法,TorF(A),如下：,TorF(A),i=0;,while (in)/n,是此,Horn,逻辑程序内子句的个数,if (,第,i,条规则的头部,=A)/,用第,i,条规则考察,A,if (,第,i,条规则的体是空的,),then return 1;,/A,是 事实,else if (TorF(A,1,)=TorF(A,m,)=1),/A,1,A,m,是第,i,条规则体内的所有原子,then return 1;/,由,i,规则推出原子,A,的正确,i=i+1;/,第,i,条规则体内并非所有原子正确，从而需,要考察别的规则,return 0;/,考察了所有的规则，都不能推出,A,4.4,谓词,Horn,逻辑中的自动推理,因为涉及到量词，谓词,Horn,逻辑的消解要复杂一些。消解方式如下。若有子句,S,1,：,A,1,A,n,S,2,：,B,1,B,m,B,，,并且,A,i,B,具有合一替换,，,则归结后的子句为,S,3,：,(A,1,A,i-1,B,1,B,m,A,i+1,A,n,),与命题,Horn,逻辑相比，需要考虑项的匹配，即合一问题。,4.4,谓词,Horn,逻辑中的自动推理,基于以上消解方式，求证一个目标,S,1,：,A,1,A,n,时，要求得出的结果应该是一个替换的集合。集合内的每一个元素,i,应该使,A,1,i,A,n,i,成立。,4.4,谓词,Horn,逻辑中的自动推理,在以一个原子,A,i,为目标进行考察时，考察每一个头部是,A,i,的子句，以此子句的体作为新的目标。返回的不是,0,（假）或者,1,（真），而应是一个替换的集合,。,为此先要给出替换算法,Substitution,以及求表达式合一算法,Unify,。,4.4,谓词,Horn,逻辑中的自动推理,将替换,作用于表达式,e,的算法如下,Substitution(e,),if(e,是常量符号,)then return e;,if(e,是变量符号,x)then if(t/x,)then return t,else return e;,if(e=f(t,1,t,n,)then t,1,=Substitution(t,1,);,t,n,=Substitution(t,n,),return f(t,1,t,n,),4.4,谓词,Horn,逻辑中的自动推理,对两个表达式,e,1,，,e,2,作合一的算法如下,/,算法返回一个合一替换或“无法合一”的信息,Unify(e,1,，,e,2,),=,空集；,if e,1,是变量符号,x then,=e,2,/x;,else if e,2,是变量符号,x then,=e,1,/x;,else if(e,1,是常量而,e,2,不是，或,e,2,是常量而,e,1,不是，,或,e,1,，,e,2,是两个不同的常量,),then return “,无法合一”,else /,此时,e,1,，,e,2,形如,f(t,1,t,n,),和,g(s,1,s,m,),；,f,g,为函数符号。,4.4,谓词,Horn,逻辑中的自动推理,if(f,g)then retu