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

计算引论第四章 推理与计算4 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，c×d-2是两个项，则gcd(a+b, c×d-2)也是项原子n若P是一个n元谓词符号，t1,…, tn是项,那么P(t1,…, tn)是原子 n例如，father是表示父子关系的二元谓词，则father(John, Peter)是原子，表示John是Peter的父亲。

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

Skolem标准型（续）n对公式P的SKOLEM化的步骤如下：（1）将P化为前束范式（Q1x1）…（Qnxn）H(x1.... xn) 其中 Q1…Qn是存在量词或者全称量词，并将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经过如上处理，可以化为x1…xn(G1…Gm) 的形式，其中G1,…,Gm都是子句省略全称量词，再用“，”取代合取符号，便得到公式P的Skolem标准型{G1,…,Gm} Skolem标准型（续）n由以上可知，任意公式都有与之相对的子句集子句集的形式是相对简单的需要注意的是，一个公式与它的Skolem标准型未必等值，但在不可满足的意义上是一致的 Horn子句与Horn逻辑程序n如果在一个子句中最多含有一个正文字，那么该子句称为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与E2的合一 替换合一替换（续）n例2，设E1与E2同上，={a/x, f(z)/y}，则 E1=g(a, f(z))=E2，所以也是E1与E2的合一替换 显然比 简单，易证=  ◦ ，其中={h(u)/z}4.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)→，即要查询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,…,AnS2：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 (i

消解方式如下若有子句S1：A1,…,An S2：B1,…,BmB， 并且Ai, B具有合一替换，则归结后的子句为S3：(A1,…,Ai-1,B1,…,Bm, Ai+1,…,An) n 与命题Horn逻辑相比，需要考虑项的匹配，即合一问题4.4 谓词谓词Horn逻辑中的自动推理逻辑中的自动推理 基于以上消解方式，求证一个目标S1：A1,…,An 时，要求得出的结果应该是一个替换的集合集合内的每一个元素i应该使A1i, …, Ani 成立4.4 谓词谓词Horn逻辑中的自动推理逻辑中的自动推理n在以一个原子Ai为目标进行考察时，考察每一个头部是Ai的子句，以此子句的体作为新的目标返回的不是0（假）或者1（真），而应是一个替换的集合Θn为此先要给出替换算法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 (fg) 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逻辑中的自动推理逻辑中的自动推理n考察某个原子A的算法TorF(A)如下 TorF(A)输入A(s1,…,sn), 返回替换数组Θ, 其中数组元素Θ[i]是一个替换 TorF(A) { i=0； Θ=空集； while(i0 // 下面i1, i2,…,im初值均为1 while(TorF(A1)[i1]!=NULL) {1=TorF(A1)[i1]; i1=i1＋1; while(TorF(A21)[i2]!=NULL) {… while(TorF(Am m-1)[im]!=NULL) {  m=TorF(A1)[im]; =  ◦ 1◦…◦ m; Θ=Θ {}； im＝ im +1; } … } } } } L1: i=i+1; //考察下一条规则 }return Θ; }。