计算引论9 推理与计算

1、计算引论第四章 推理与计算4 推理与计算n预 备 知 识 nHorn逻辑程序n命题Horn逻辑中的自动推理n谓词Horn逻辑中的自动推理 4.1 预备知识n考虑到读者已学习数理逻辑，基本熟悉 相关概念和知识，下面我们简单给出有 关逻辑推理的基本概念。因为篇幅所限 ，为理解更加形象，概念定义形式未必 采用数理逻辑中严格定义形式，准确概 念请参见离散数学数理逻辑部分。命题 n在一阶逻辑中，命题陈述某个对象的性 质，或是某些对象的关系。陈述的形式 是作为n元函数的“谓词”与它的变量“项” 。n例如命题“鸟会飞”表示为canfly(bird)， 其中“canfly”是谓词，“bird”是项。 项n项是指某个命题的“对象”或是“客体”。如 下递归定义“项”i单个的常量和变量都是项。 ii如果f是函数符, t1, tn是项，那么 f(t1, tn)也是项。n例如，gcd是表示最大公约数的函数符， a+b，cd-2是两个项，则gcd(a+b, cd- 2)也是项。原子n若P是一个n元谓词符号，t1, tn是项,那 么P(t1, tn)是原子 n例如，father是表示父子关系的二元谓词 ，则fath

2、er(John, Peter)是原子，表示 John是Peter的父亲。这里 father(John, Peter)做为基本二元关系。公式n如下递归定义“公式”i原子是公式ii若P,Q是公式，则PQ, PQ, PQ, P 是公式iii若P是公式，x是P中的变量，则(x)P，(x)P 是公式。 文字和子句n若P是原子，则P, P称为文字。P称为正文字 ，P称为负文字。n公式P称为子句，若P等值于L1Ln，其中 L1,Ln是文字。n没有变量符号出现的项、原子、子句， 分别称 为基项、基原子、基子句。文字和子句（续）n例如，gcd(45, b)是基项father(John, Peter)是基原子father(John, Peter) uncle(John, Peter)是基子句Skolem标准型n上面定义的公式，形式是很多样的。这就会给机器的形式化处理带来很大的麻烦。为了便于机器处理，需要把公式化成统一的标准形式，即SKOLEM标准型，进而建立子句集。 Skolem标准型（续）n设P是公式，P等价于x1xnG(x1 xn)，并且GG1Gm，其中G1,Gm都是子句，则称G的子句集S=G1,Gm

3、为公式P的Skolem标准型。Skolem标准型（续）n对公式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标准型（续）n公式P经过如上处理，可以化为x1xn(G1Gm)的形式，其中G1,Gm都是子句。省略全称量词，再用“，”取代合取符号，便得到公式P的Skolem标准型G1,Gm 。 Skolem标准型（续）n由以上可知，任意公式都有与之相对的子句集。子句集的形式是相对简单的。需要注意的是，一个公式与它的Skolem标准型未必等值，但在不可满足的意义上是一致的。 Horn子句与Horn逻辑程序n如果在一个子

4、句中最多含有一个正文字，那么该子句称为Horn子句。n若一个子句集内的子句个数有限且都是 Horn子句，那么该子句集称为一个Horn逻 辑程序。替换n一个替换是形如t1/x1, tn/xn的一个有限集合。其中xi（i=1,n） 是两两不同的变量符号, ti是不同于xi的项。替换可以如下作用于一个表达式：给定替换=t1/x1, tn/xn和表达式E，E表示将E中出现的每一个xi（i=1,n）都替换成ti得到的新表达式。 替换（续）n给定两个替换=t1/x1, tn/xn =u1/y1, um/ym将集合 t1/x1, tn /xn ,u1/y1, um/ym 删去以下元素：n ui/yi，当yi x1, xn n ti /xi，当ti =xi得到的新替换表示为 ，称为 和 的复合 。 合一替换n给定表达式E1,Ek，若存在替换 ，使得E1=Ek ，则称是E1,Ek的一个合一替换。 合一替换（续）n 例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与

5、E2的合一替换。合一替换（续）n例2，设E1与E2同上，=a/x, f(z)/y，则 E1=g(a, f(z)=E2，所以也是E1与E2的合一替换。显然比 简单，易证= ，其中=h(u)/z4.2 Horn逻辑程序n在知识工程中，知识要作为数据按一定格式存 放在数据库中。n已知的知识表示方法有n产生式表示法n语义网络表示法n逻辑表示法n产生式表示法是一类很重要的方法，知识表示 成IF THEN 的形式。采用产生式方法，可 以将规则与事实以统一的格式表示，即Horn子 句。4.2 Horn逻辑程序nHorn子句可以表示成如下形式：规则体规则头其中规则体一般是n个原子的合取， n=0,1,。规则头可以是单个原子，也可以是空。4.2 Horn逻辑程序在Horn逻辑程序自动推理时用到如下概念：n规则：规则体非空且规则头非空的子句。例如 ，father(z, y), father(y, x)grandfather(z, x)n事实：规则体空且规则头非空的子句。例如， father(John, Peter)。n目标：无规则头的子句，例如， grandfather(Smith, Peter)，即要查

6、询Smith 是否是Peter的祖父？4.2 Horn逻辑程序n一个Horn逻辑程序是Horn子句的集合，也就是规则和事实的集合。因此，一个Horn逻辑程序相当于一个知识库。n知识库应当具有自动推理的能力。所谓推理，实际上是通过对一组子句按照一定的方式进行消解最终得到新的公式。4.2 Horn逻辑程序n自动推理的过程即给定目标子句，机器按照一定的顺序对逻辑程序中的子句进行消解，最后得到目标子句，或者得出目标不可满足的结论。4.2 Horn逻辑程序n因为Horn子句结构特殊，Horn逻辑程序上的消解过程简单。下面分别在命题Horn逻辑和谓词Horn逻辑情形下给出消解过程。 4.3 命题Horn逻辑中的自动推理 n在命题Horn逻辑中，子句之间可以按照如下的 方式消解。若有子句S1：A1,AnS2：B1,Bm Ai 则归结后的子句为S3：A1,Ai-1, B1,Bm, Ai+1,An 即利用规则S2将原目标S1转化为新目标S3.4.3 命题Horn逻辑中的自动推理n基于上述消解方式，求证一个目标 S：A1,An 需要逐一以S的体中的每一个原子Ai作为新的目 标进行求证。 A1,An 也称为S的子目标。n在以一个原子Ai为目标进行求证时，考察子句集 内所有头部是Ai的子句，以此子句的体作为新的 目标。 4.3 命题Horn逻辑中的自动推理n当某个关于A的子句体部的所有原子得到满足时，直接返回A是正确的，而不用再接着考察头是A的其他子句。n假如对于某个原子A，逻辑程序中所有头部是A的子句都无法满足，则得出A无法满足的结论。 原子A的推理算法TorF(A)如下： TorF(A) i=0;while (i0/ 下面i1, i2,im初值均为1while(TorF(A1)i1!=NULL)1=TorF(A1)i1; i1=i11;while(TorF(A21)i2!=NULL)while(TorF(Am m-1)im!=NULL) m=TorF(A1)im;= 1 m;= ；im im +1; L1: i=i+1; /考察下一条规则 return ;

《计算引论9 推理与计算》由会员kms****20分享，可在线阅读，更多相关《计算引论9 推理与计算》请在金锄头文库上搜索。