计算引论 推理与计算

计算引论推理与计算第一页，共六十四页，2022年，8月28日主要内容逻辑与推理Horn逻辑程序命题Horn逻辑中的自动推理谓词Horn逻辑中的自动推理

Prolog逻辑

程序设计第二页，共六十四页，2022年，8月28日4.1逻辑基础知识符号表示：常量：小写字母a,b,c,...。函数：小写字母f,g,h,...。变量：小写字母x,y,z,...。逻辑算子(或连结词)：,,,→,↔。量词：,.谓词：大写字母P,Q,R,...。第三页，共六十四页，2022年，8月28日4.1逻辑基础知识命题：在一阶逻辑中，命题陈述某个对象的性质，或是某些对象的关系，是能够分辨真假的语句。原子命题：一个语句如果不能再进一步分解成更简单的语句，并且又是一个命题，则称此命题为原子命题第四页，共六十四页，2022年，8月28日命题公式：原子命题是命题公式。若A是命题公式，则A也是命题公式。若A和B都是命题公式，则A∧B、A∨B、

A→B、A↔B是命题公式。

第五页，共六十四页，2022年，8月28日命题公式的缺点：无法把所描述的客观事物的结构和逻辑特征反映出来不能把不同事物的共同特征反映出来例如：命题P:“张三是李四的老师”第六页，共六十四页，2022年，8月28日谓词逻辑：在谓词逻辑中，将原子命题分解为谓词与个体两部分。个体是指可以独立存在的物体，可以是抽象的或具体的。谓词则是用于刻画个体的性质、状态或个体间的关系的。第七页，共六十四页，2022年，8月28日

谓词的一般形式：P(x1,x2,…,xn)其中P是谓词，x1,x2,…,xn是个体。例：“鸟会飞”可表示为canfly(bird).其中canfly是谓词，bird是个体。

第八页，共六十四页，2022年，8月28日谓词分类：一元谓词：刻画个体的性质多元谓词：刻画个体之间的关系一阶谓词：个体是常量、变元高阶谓词：个体是谓词第九页，共六十四页，2022年，8月28日项定义如下：单个的常量和变量都是项。如果f是函数符,t1,…,tn是项，那么f(t1,…,tn)也是项。

例如，gcd是表示最大公约数的函数符，a+b，c×d-2是两个项，则gcd(a+b,cd-2)也是项。第十页，共六十四页，2022年，8月28日原子：

若P是一个n元谓词符号，t1,…,tn是项,那么P(t1,…,tn)是原子。例如，father是表示父子关系的二元谓词，则father(John,Peter)是原子，表示John是Peter的父亲。这里father(John,Peter)做为基本二元关系。第十一页，共六十四页，2022年，8月28日谓词公式：

原子是公式

若P,Q是公式，则P→Q,P↔Q,P∧Q,P∨Q,P是公式。

若P是公式，x是P中的变量，则(x)P，(x)P是公式。第十二页，共六十四页，2022年，8月28日文字：

若P是原子，则P,P称为文字。P称为正文字，P称为负文字。子句：

公式P称为子句，若P为L1…Ln，其中L1,…,Ln是文字。基项、基原子、基子句：没有变量符号出现的项、原子、子句，分别称为基项、基原子、基子句。第十三页，共六十四页，2022年，8月28日例:gcd(45,b)是基项

father(John,Peter)是基原子father(John,Peter)uncle(John,Peter)是基子句第十四页，共六十四页，2022年，8月28日谓词公式的解释

设D为谓词公式P的个体域，若对P中的个体常量、函数和谓词按照如下规定赋值：（1）为每个个体常量指派D中的一个元素；（2）为每个n元函数指派一个从Dn到D的映射，其中

Dn={(x1,x2,…,xn)|x1,x2,…,xn

D}（3）为每个n元谓词指派一个从Dn到{F,T}的映射；则称这些指派为公式P在D上的一个解释。第十五页，共六十四页，2022年，8月28日永真：如果谓词公式P，对个体域D上的任何一个解释都取得真值T，则称P在D上是永真的。如果P在每个非空个体域上均永真，则称P永真。第十六页，共六十四页，2022年，8月28日永假（不可满足性）如果谓词公式P对于个体域D上的所有解释都取得假值F，则称P在D上是永假的；如果P在每个非空个体域上均永假，则称P永假。第十七页，共六十四页，2022年，8月28日可满足的：对于谓词公式P，如果至少存在一个解释使得公式P在此解释下的真值为T，则称公式P是可满足的。不可满足的：对谓词公式P，如果不存在任何解释，使得P的取值为T，则称公式P是不可满足的。第十八页，共六十四页，2022年，8月28日4.2推理相关知识推理：指从已知事实出发，运用已掌握的知识，推导出其中蕴含的事实性结论或归纳出某些新的结论的过程。推理分类：自然演绎：已知事实推理规则结论归结：否定结论前提条件矛盾第十九页，共六十四页，2022年，8月28日Skolem化：

公式形式是很多样的。这就会给机器的形式化处理带来很大的麻烦。为了便于机器处理，把公式化成统一的标准形式，即SKOLEM标准型。第二十页，共六十四页，2022年，8月28日Skolem标准型：

设P是公式，P等价于x1…xnG(x1....xn)，并且G＝G1…Gm，其中G1,…,Gm都是子句，则称G的子句集S={G1,…,Gm}为公式P的Skolem标准型。第二十一页，共六十四页，2022年，8月28日对公式P的SKOLEM化的步骤如下：（1）将P化为前束范式（Q1x1）…（Qnxn）H(x1....xn)其中Q1…Qn是存在量词或者全称量词，H为合取范式的形式,不含→,↔；第二十二页，共六十四页，2022年，8月28日（2）用如下方法消去存在量词：i)若Qi是一个存在量词，并且它的左边没有全称量词，则用一个H中没有的常量符号代替H中所有的xi，之后消去（Qixi）

第二十三页，共六十四页，2022年，8月28日ii)若Qi是一个存在量词，并且Qj1,…Qjk是Qi左边的全称量词，则取一个H中没有的函数k元符号f,用f(xj1,…,xjk)代替xi,之后消去（Qixi）。第二十四页，共六十四页，2022年，8月28日公式P经过如上处理，可以化为x1…xn(G1…Gm)的形式，其中G1,…,Gm都是子句。省略全称量词，再用“，”取代合取符号，便得到公式P的Skolem标准型{G1,…,Gm}。

第二十五页，共六十四页，2022年，8月28日任意公式都有与之相对的子句集。一个公式与它的Skolem标准型未必等值，但在不可满足的意义上是一致的。第二十六页，共六十四页，2022年，8月28日置换：是形如{t1/x1,…,tn/xn}的一个有限集合。其中xi（i=1,…,n）是两两不同的变量符号,ti是不同于xi的项。置换作用于表达式：

给定置换={t1/x1,…,tn/xn}和表达式E，E表示将E中出现的每一个xi（i=1,…,n）都替换成ti得到的新表达式。第二十七页，共六十四页，2022年，8月28日给定两个置换={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

得到的新置换表示为·

，称为和

的复合。第二十八页，共六十四页，2022年，8月28日

置换满足结合律

(·

)·

=·(·

)

置换不满足交换律

·

·

·=·=第二十九页，共六十四页，2022年，8月28日合一置换：

给定表达式E1,…,Ek，若存在置换，使得E1=…=Ek

，则称是E1,…,Ek的一个合一置换。

第三十页，共六十四页，2022年，8月28日

例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的合一置换。第三十一页，共六十四页，2022年，8月28日例2，设E1与E2同上，={a/x,f(z)/y}，则E1=g(a,f(z))=E2，所以也是E1与E2的合一置换。显然比简单，易证=◦，其中={h(u)/z}第三十二页，共六十四页，2022年，8月28日

最一般合一置换求法：设有公式：E1=P(x,y,z);E2=

P(x,f(a),g(b))从左至右查找不同的项，构成了不一致集：

D1={y,f(a)}继续向右比较又得到一个不一致集：D2={z,g(b)}置换为={f(a)/y,g(b)/z}第三十三页，共六十四页，2022年，8月28日

求一般置换算法：令W={E1,E2}令k=0,Wk=W,σk=ε;ε是空置换,表示不作置换。如果Wk只有一个表达式，则算法停止，σk就是所要求的结果.找出Wk的不一致集Dk

。若Dk中存在元素xk和tk

，其中xk是变元，tk是项，且xk不在tk中出现，则：σk+1=σk·{tk/xk}Wk+1=wk{tk/xk}k=k+1然后转（2）。算法终止，W的一般合一置换不存在。第三十四页，共六十四页，2022年，8月28日可以证明，如果E1和E2可合一，则算法必停止于第2步。第三十五页，共六十四页，2022年，8月28日4.2Horn逻辑程序人工智能：

知识库：用于推理的知识

数据库：事实和论据

推理：对知识和数据的消解，获得结论第三十六页，共六十四页，2022年，8月28日4.2Horn逻辑程序已知的知识表示方法有产生式表示法语义网络表示法逻辑表示法产生式表示法是一类很重要的方法，知识表示成IF…THEN…的形式。采用产生式方法，可以将规则与事实以统一的格式表示，即Horn子句。第三十七页，共六十四页，2022年，8月28日4.2Horn逻辑程序如果在一个子句中最多含有一个正文字，那么该子句称为Horn子句。若一个子句集内的子句个数有限且都是Horn子句，那么该子句集称为一个Horn逻辑程序。第三十八页，共六十四页，2022年，8月28日4.2Horn逻辑程序Horn子句可以表示成如下形式：规则体→规则头其中规则体一般是n个原子的合取，n=0,1,…。规则头可以是单个原子，也可以是空。第三十九页，共六十四页，2022年，8月28日4.2Horn逻辑程序规则：规则体非空且规则头非空的子句。例如，

father(z,y),father(y,x)→grandfather(z,x)事实：规则体空且规则头非空的子句。例如，→father(John,Peter)。目标：无规则头的子句，例如，grandfather(Smith,Peter)→，即要查询Smith是否是Peter的祖父？第四十页，共六十四页，2022年，8月28日4.2Horn逻辑程序一个Horn逻辑程序是Horn子句的集合，也就是规则和事实的集合。因此，一个Horn逻辑程序相当于一个知识库。推理即是通过对一组子句按照一定的方式进行消解最终得到新的公式。第四十一页，共六十四页，2022年，8月28日自动推理的过程即给定目标子句，机器按照一定的顺序对逻辑程序中的子句进行消解，最后得到目标子句，或者得出目标不可满足的结论。第四十二页，共六十四页，2022年，8月28日命题Horn逻辑的自动推理谓词Horn逻辑的自动推理第四十三页，共六十四页，2022年，8月28日4.3命题Horn逻辑中的自动推理在命题Horn逻辑中，子句之间可以按照如下的方式消解。若有子句S1：A1,…,AnS2：B1,…,Bm

Ai则归结后的子句为

S3：A1,…,Ai-1,B1,…,Bm,Ai+1,…,An

即利用规则S2将原目标S1转化为新目标S3.第四十四页，共六十四页，2022年，8月28日4.3命题Horn逻辑中的自动推理基于上述消解方式，求证一个目标S：A1,…,An

需要逐一以S的体中的每一个原子Ai作为新的目标进行求证。A1,…,An也称为S的子目标。在以一个原子Ai为目标进行求证时，考察子句集内所有头部是Ai的子句，以此子句的体作为新的目标。第四十五页，共六十四页，2022年，8月28日4.3命题Horn逻辑中的自动推理当某个关于A的子句体部的所有原子得到满足时，直接返回A是正确的，而不用再接着考察头是A的其他子句。假如对于某个原子A，逻辑程序中所有头部是A的子句都无法满足，则得出A无法满足的结论。第四十六页，共六十四页，2022年，8月28日原子A的推理算法TorF(A)如下：TorF(A){i=0;while(i<n)//n是此Horn逻辑程序内子句的个数

{if(第i条规则的头部=A)//用第i条规则考察A{if(第i条规则的体是空的)thenreturn1;//A是事实

elseif(TorF(A1)=…=TorF(Am)=1)//A1…Am是第i条规则体内的所有原子thenreturn1;//由i规则推出原子A的正确}i=i+1;//第i条规则体内并非所有原子正确，从而需要考察别的规则

}return0;//考察了所有的规则，都不能推出A}第四十七页，共六十四页，2022年，8月28日4.4谓词Horn逻辑中的自动推理谓词Horn逻辑的消解要复杂一些。消解方式如下。若有子句S1：A1,…,An

S2：B1,…,BmB，并且Ai,B具有合一置换，则归结后的子句为S3：(A1,…,Ai-1,B1,…,Bm,Ai+1,…,An)

与命题Horn逻辑相比，需要考虑项的匹配，即合一问题。第四十八页，共六十四页，2022年，8月28日4.4谓词Horn逻辑中的自动推理基于以上消解方式，求证一个目标S1：A1,…,An

时，要求得出的结果应该是一个置换的集合。集合内的每一个元素i应该使A1i,…,Ani成立。第四十九页，共六十四页，2022年，8月28日4.4谓词Horn逻辑中的自动推理在以一个原子Ai为目标进行考察时，考察每一个头部是Ai的子句，以此子句的体作为新的目标。返回的不是0（假）或者1（真），而应是一个置换的集合Θ。为此先要给出置换算法Substitution以及求表达式合一算法Unify。第五十页，共六十四页，2022年，8月28日

4.4谓词Horn逻辑中的自动推理将置换作用于表达式e的算法如下Substitution(e,){if(e是常量符号)thenreturne;if(e是变量符号x)then{if(t/x)thenreturntelsereturne;}if(e=f(t1,…,tn))then{t1=Substitution(t1,);…tn=Substitution(tn,)returnf(t1,…,tn)}}第五十一页，共六十四页，2022年，8月28日4.4谓词Horn逻辑中的自动推理对两个表达式e1，e2作合一的算法如下//算法返回一个合一置换或“无法合一”的信息Unify(e1，e2){=空集；ife1是变量符号xthen={e2/x};elseife2是变量符号xthen={e1/x};elseif(e1是常量而e2不是，或e2是常量而e1不是，或e1，e2是两个不同的常量)thenreturn“无法合一”else//此时e1，e2形如f(t1,…,tn)和g(s1,…,sm)；f,g为函数符号。第五十二页，共六十四页，2022年，8月28日4.4谓词Horn逻辑中的自动推理

{if(fg)thenreturn“无法合一”;else{

1=Unify(t1，s1);

=◦

1;

2=Unify(Substitution(t2,),Substitution(s2,));

=◦

2;…

n=Unify(Substitution(tn,)，Substitution(sn,));

=◦

n;return;}}}第五十三页，共六十四页，2022年，8月28日4.4谓词Horn逻辑中的自动推理例：Horn逻辑程序（知识库）如下，father(z,y),father(y,x)→grandfather(z,x)，→father(John,Peter)，→father(Smith,John)。

目标为grandfather(Smith,Peter)→，即查询Smith是否是Peter的祖父？第五十四页，共六十四页，2022年，8月28日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}

第五十五页，共六十四页，2022年，8月28日4.4谓词Horn逻辑中的自动推理考察某个原子A的算法TorF(A)如下

TorF(A)输入A(s1,…,sn),返回置换数组Θ,其中数组元素Θ[i]是一个置换。第五十六页，共六十四页，2022年，8月28日

TorF(A){i=0；

Θ=空集；

while(i<n)//n是此Horn逻辑程序内子句的个数

{if(第i条规则的头部=A(t1,…,tn)//t1,..,tn是项) {//用第i条规则考察A

=Unify(A(t1,…,tn),A(s1,…,sn))；

if=“无法合一”,gotoL1if(第i条规则的体是空的，即事实) thenΘ=Θ{}；

else{//A1…Am是第i条规则体内所有原子，m>0//下面i1,i2,…,im初值均为1while(TorF(A1)[i1]!=NULL){1=TorF(A1)[i1];i1=i1＋1;第五十七页，共六十四页，2022年，8月28日while(TorF(A21)[i2]!=NULL){…while(TorF(Am

m-1)[im]!=NULL){

m=TorF(A1)[im];

=

◦

1◦…◦

m;Θ=Θ{}；

im＝im

+1;}…}}}}L1 :i