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

《计算引论9 推理与计算.ppt》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、计算引论第四章推理与计算4推理与计算预备知识Horn逻辑程序命题Horn逻辑中的自动推理谓词Horn逻辑中的自动推理4.1预备知识考虑到读者已学习数理逻辑，基本熟悉相关概念和知识，下面我们简单给出有关逻辑推理的基本概念。因为篇幅所限，为理解更加形象，概念定义形式未必采用数理逻辑中严格定义形式，准确概念请参见离散数学数理逻辑部分。命题在一阶逻辑中，命题陈述某个对象的性质，或是某些对象的关系。陈述的形式是作为n元函数的“谓词”与它的变量“项”。例如命题“鸟会飞”表示为canfly(bird)，其中“canfly”是谓词，“b

2、ird”是项。项项是指某个命题的“对象”或是“客体”。如下递归定义“项”i〕单个的常量和变量都是项。ii〕如果f是函数符,t1,…,tn是项，那么f(t1,…,tn)也是项。例如，gcd是表示最大公约数的函数符，a+b，c×d-2是两个项，则gcd(a+b,c×d-2)也是项。原子若P是一个n元谓词符号，t1,…,tn是项,那么P(t1,…,tn)是原子例如，father是表示父子关系的二元谓词，则father(John,Peter)是原子，表示John是Peter的父亲。这里father(John,Peter)做为基本

3、二元关系。公式如下递归定义“公式”i〕原子是公式ii〕若P,Q是公式，则P→Q,P∧Q,P∨Q,P是公式iii〕若P是公式，x是P中的变量，则(x)P，(x)P是公式。文字和子句若P是原子，则P,P称为文字。P称为正文字，P称为负文字。公式P称为子句，若P等值于L1…Ln，其中L1,…,Ln是文字。没有变量符号出现的项、原子、子句，分别称为基项、基原子、基子句。文字和子句（续）例如，gcd(45,b)是基项father(John,Peter)是基原子father(John,Peter)uncle(John

4、,Peter)是基子句Skolem标准型上面定义的公式，形式是很多样的。这就会给机器的形式化处理带来很大的麻烦。为了便于机器处理，需要把公式化成统一的标准形式，即SKOLEM标准型，进而建立子句集。Skolem标准型（续）设P是公式，P等价于x1…xnG(x1....xn)，并且G＝G1…Gm，其中G1,…,Gm都是子句，则称G的子句集S={G1,…,Gm}为公式P的Skolem标准型。Skolem标准型（续）对公式P的SKOLEM化的步骤如下：（1）将P化为前束范式（Q1x1）…（Qnxn）H(x1....xn

5、)其中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标准型（续）公式P经过如上处理，可以化为x1…xn(G1…Gm)的形式，其中G1,

6、…,Gm都是子句。省略全称量词，再用“，”取代合取符号，便得到公式P的Skolem标准型{G1,…,Gm}。Skolem标准型（续）由以上可知，任意公式都有与之相对的子句集。子句集的形式是相对简单的。需要注意的是，一个公式与它的Skolem标准型未必等值，但在不可满足的意义上是一致的。Horn子句与Horn逻辑程序如果在一个子句中最多含有一个正文字，那么该子句称为Horn子句。若一个子句集内的子句个数有限且都是Horn子句，那么该子句集称为一个Horn逻辑程序。替换一个替换是形如{t1/x1,…,tn/xn}的一个有限集

7、合。其中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得到的新替换表示为◦，称为和的复合。合一替换给

8、定表达式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，所以是E