计算引论9推理与计算.ppt

计算引论,第四章 推理与计算,4 推理与计算,预 备 知 识 Horn逻辑程序 命题Horn逻辑中的自动推理 谓词Horn逻辑中的自动推理,4.1 预备知识,考虑到读者已学习数理逻辑，基本熟悉相关概念和知识，下面我们简单给出有关逻辑推理的基本概念。因为篇幅所限，为理解更加形象，概念定义形式未必采用数理逻辑中严格定义形式，准确概念请参见离散数学数理逻辑部分。,命题,在一阶逻辑中，命题陈述某个对象的性质，或是某些对象的关系。陈述的形式是作为n元函数的“谓词”与它的变量“项”。 例如命题“鸟会飞”表示为canfly(bird)，其中“canfly”是谓词，“bird”是项。,项,项是指某个命题的“对象”或是“客体”。如下递归定义“项” i单个的常量和变量都是项。 ii如果f是函数符, t1, tn是项，那么 f(t1, tn)也是项。 例如，gcd是表示最大公约数的函数符，a+b，cd-2是两个项，则gcd(a+b, cd-2)也是项。,原子,若P是一个n元谓词符号，t1, tn是项,那么P(t1, tn)是原子 例如，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等值于L1Ln，其中L1,Ln是文字。 没有变量符号出现的项、原子、子句， 分别称为基项、基原子、基子句。,文字和子句（续）,例如，gcd(45, b)是基项 father(John, Peter)是基原子 father(John, Peter) uncle(John, Peter) 是基子句,Skolem标准型,上面定义的公式，形式是很多样的。这就会给机器的形式化处理带来很大的麻烦。为了便于机器处理，需要把公式化成统一的标准形式，即SKOLEM标准型，进而建立子句集。,Skolem标准型（续）,设P是公式，P等价于x1xnG(x1 xn)，并且GG1Gm，其中G1,Gm都是子句，则称G的子句集 S=G1,Gm 为公式P的Skolem标准型。,Skolem标准型（续）,对公式P的SKOLEM化的步骤如下： （1）将P化为前束范式 （Q1x1）（Qnxn）H(x1 xn) 其中 Q1Qn是存在量词或者全称量词，并将H化为合取范式的形式；,Skolem标准型（续）,（2）用如下方法消去存在量词： i) 若Qi是一个存在量词，并且它的左边没有全称量词，则用一个H中没有的常量符号代替H中所有的xi，之后消去（Qixi）,Skolem标准型（续）,ii) 若Qi是一个存在量词，并且Qj1,Qjk是Qi左边的全称量词，则取一个H中没有的函数k元符号f, 用f(xj1,xjk)代替xi,之后消去（Qixi）。,Skolem标准型（续）,公式P经过如上处理，可以化为 x1xn(G1Gm) 的形式，其中G1,Gm都是子句。省略全称量词，再用“，”取代合取符号，便得到公式P的Skolem标准型G1,Gm 。,Skolem标准型（续）,由以上可知，任意公式都有与之相对的子句集。子句集的形式是相对简单的。需要注意的是，一个公式与它的Skolem标准型未必等值，但在不可满足的意义上是一致的。,Horn子句与Horn逻辑程序,如果在一个子句中最多含有一个正文字，那么该子句称为Horn子句。 若一个子句集内的子句个数有限且都是Horn子句，那么该子句集称为一个Horn逻辑程序。,替换,一个替换是形如t1/x1, tn/xn的一个有限集合。其中xi（i=1,n） 是两两不同的变量符号, ti是不同于xi的项。 替换可以如下作用于一个表达式：给定替换=t1/x1, tn/xn和表达式E，E表示将E中出现的每一个xi（i=1,n）都替换成ti得到的新表达式。,替换（续）,给定两个替换 =t1/x1, tn/xn =u1/y1, um/ym 将集合 t1/x1, tn /xn ,u1/y1, um/ym 删去以下元素： ui/yi，当yi x1, xn ti /xi，当ti =xi 得到的新替换表示为 ，称为 和 的复合 。,合一替换,给定表达式E1,Ek，若存在替换 ，使得E1=Ek ，则称是E1,Ek的一个合一替换。,合一替换（续）,例1，设E1=g(x,y)，E2=g(a,f(z)。令 =a/x, f(h(u)/y, h(u)/z， 则E1=g(a, f(h(u), E2=g(a, f(h(u) 因为E1=E2，所以是E1与E2的合一 替换。,合一替换（续）,例2，设E1与E2同上，=a/x, f(z)/y，则 E1=g(a, f(z)=E2，所以也是E1与E2的合一替换。 显然比 简单，易证= ，其中=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逻辑中，子句之间可以按照如下的方式消解。若有子句 S1：A1,An S2：B1,Bm Ai 则归结后的子句为 S3：A1,Ai-1, B1,Bm, Ai+1,An 即利用规则S2将原目标S1转化为新目标S3.,4.3 命题Horn逻辑中的自动推理,基于上述消解方式，求证一个目标 S：A1,An 需要逐一以S的体中的每一个原子Ai作为新的目标进行求证。 A1,An 也称为S的子目标。 在以一个原子Ai为目标进行求证时，考察子句集内所有头部是Ai的子句，以此子句的体作为新的目标。,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(A1)= = TorF(Am)=1) /A1 Am 是第i条规则体内的所有原子 then return 1; /由i规则推出原子A的正确 i=i+1; /第i条规则体内并非所有原子正确，从而需 要考察别的规则 return 0; /考察了所有的规则，都不能推出A ,4.4 谓词Horn逻辑中的自动推理,因为涉及到量词，谓词Horn逻辑的消解要复杂一些。消解方式如下。若有子句 S1：A1,An S2：B1,BmB， 并且Ai, B具有合一替换，则归结后的子句为 S3：(A1,Ai-1,B1,Bm, Ai+1,An) 与命题Horn逻辑相比，需要考虑项的匹配，即合一问题。,4.4 谓词Horn逻辑中的自动推理,基于以上消解方式，求证一个目标 S1：A1,An 时，要求得出的结果应该是一个替换的集合。集合内的每一个元素i应该使 A1i, , Ani 成立。,4.4 谓词Horn逻辑中的自动推理,在以一个原子Ai为目标进行考察时，考察每一个头部是Ai的子句，以此子句的体作为新的目标。返回的不是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(t1,tn) then t1= Substitution(t1, ); tn= Substitution(tn, ) return f(t1,tn) ,4.4 谓词Horn逻辑中的自动推理,对两个表达式e1，e2作合一的算法如下 /算法返回一个合一替换或“无法合一”的信息 Unify(e1，e2) =空集； if e1是变量符号x then = e2/x; else if e2是变量符号x then = e1/x; else if(e1是常量而e2不是，或e2是常量而e1不是， 或 e1，e2是两个不同的常量) then return “无法合一” else /此时e1，e2形如f(t1,tn)和 g(s1,sm)；f,g为函数符号。,4.4 谓词Horn逻辑中的自动推理, if (fg) then return “无法合一”; else 1= Unify(t1，s1); = 1; 2= Unify(Substitution(t2, ), Substitution(s2, ); = 2; n= Unify(Substitution(tn, )，Substitution(sn, ); = n; return ; ,4.4 谓词Horn逻辑中的自动推理,例：Horn逻辑程序（知识库）如下， father(z, y), father(y, x)grandfather(z, x)， father(John, Peter)， father(Smith, John)。 目标为grandfather(Smith, Peter)，即查询Smith是否是Peter的祖父？,4.4 谓词Horn逻辑中的自动推理,推理过程如下； 1. 首先通过合一替换=Peter/x, Smith/z，将目标与知识库中第一条规则的规则头匹配，得到新目标 father(Smith, y), father(y, Peter) 2. 考察知识库中第二条和第三条规则，通过合一替换=John/y与知识库中的事实匹配 father(Smith, John), father(John, Peter) 因此查询目标成立，并且返回替换 =Peter/x, John/y, Smith/z,4.4 谓词Horn逻辑中的自动推理,考察某个原子A的算法To