北航 计算理论 第四章 推理与计算

1、计算理论计算理论 第四章第四章 推理与计算推理与计算 主要内容主要内容 n逻辑与推理逻辑与推理 nHorn逻辑程序逻辑程序 n命题命题Horn逻辑中的自动推理逻辑中的自动推理 n谓词谓词Horn逻辑中的自动推理逻辑中的自动推理 n Prolog逻辑逻辑 程序设计程序设计 4.1 逻辑基础知识逻辑基础知识 n符号表示：符号表示： n常量常量：小写字母：小写字母 a, b, c,.。 n函数函数：小写字母：小写字母 f, g, h,. 。 n变量变量：小写字母：小写字母 x, y, z,.。 n逻辑算子逻辑算子(或连结词或连结词)： , , , , 。 n量词量词： , . n谓词谓词：大写字母：

2、大写字母 P, Q, R,. 。 4.1 逻辑基础知识逻辑基础知识 n命题命题：在一阶逻辑中，命题陈述某个对象的性：在一阶逻辑中，命题陈述某个对象的性 质，或是某些对象的关系，是能够分辨真假的质，或是某些对象的关系，是能够分辨真假的 语句。语句。 n原子命题原子命题：一个语句如果不能再进一步分解成：一个语句如果不能再进一步分解成 更简单的语句，并且又是一个命题，则称此命更简单的语句，并且又是一个命题，则称此命 题为题为原子命题原子命题 n命题公式命题公式： n原子命题是命题公式。原子命题是命题公式。 n若若A是命题公式，则是命题公式，则 A也是命题公式。也是命题公式。 n若若A和和B都是命题公

3、式，则都是命题公式，则AB、AB、 A B、AB是命题公式。是命题公式。 n命题公式的缺点：命题公式的缺点： n无法把所描述的客观事物的结构和逻辑特征无法把所描述的客观事物的结构和逻辑特征 反映出来反映出来 n不能把不同事物的共同特征反映出来不能把不同事物的共同特征反映出来 n例如：例如： 命题命题P:“张三是李四的老师张三是李四的老师” n谓词逻辑谓词逻辑： 在谓词逻辑中，将原子命题分解为谓词与在谓词逻辑中，将原子命题分解为谓词与 个体两部分。个体两部分。 n个体是指可以独立存在的物体，可以是抽象个体是指可以独立存在的物体，可以是抽象 的或具体的。的或具体的。 n谓词则是用于刻画个体的性质、

4、状态或个体谓词则是用于刻画个体的性质、状态或个体 间的关系的。间的关系的。 n 谓词的一般形式：谓词的一般形式： nP(x1,x2,xn ) 其中其中P是谓词，是谓词，x1,x2,xn是个体。是个体。 n例：例：“鸟会飞鸟会飞”可表示为可表示为canfly(bird).其其 中中canfly是谓词，是谓词，bird是个体。是个体。 n谓词分类谓词分类： n一元谓词：刻画个体的性质一元谓词：刻画个体的性质 n多元谓词：刻画个体之间的关系多元谓词：刻画个体之间的关系 n一阶谓词：个体是常量、变元一阶谓词：个体是常量、变元 n高阶谓词：个体是谓词高阶谓词：个体是谓词 n项项定义如下：定义如下： n单

5、个的常量和变量都是项。单个的常量和变量都是项。 n如果如果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是表示父子关系的二元谓词，则是表示父子关系的二元谓词，则 father(John, Peter)是原子，表示是原子，表示John是是Pete

6、r 的父亲。这里的父亲。这里 father(John, Peter)做为基本二做为基本二 元关系。元关系。 n谓词公式谓词公式： n 原子是公式原子是公式 n 若若P,Q是公式，则是公式，则 PQ, PQ, PQ, PQ, P 是公式。是公式。 n 若若P是公式，是公式，x是是P中的变量，则中的变量，则 ( x)P，( x)P 是公式。是公式。 n文字文字： 若若P是原子，则是原子，则P, P称为称为文字文字。P称为正文字，称为正文字， P称为负文字。称为负文字。 n子句子句： 公式公式P称为称为子句子句，若，若P为为L 1 L n ， 其中其中 L1,Ln是文字。是文字。 n基项、基原子、基

7、子句：基项、基原子、基子句： 没有变量符号出现的项、原子、子句，没有变量符号出现的项、原子、子句， 分别分别 称为称为基项、基原子、基子句。基项、基原子、基子句。 n例例: gcd(45, b)是基项是基项 father(John, Peter)是基原子是基原子 father(John, Peter) uncle(John, Peter) 是基子句是基子句 n谓词公式的解释谓词公式的解释 设设D为谓词公式为谓词公式P的个体域，若对的个体域，若对P中的个体常量、函数中的个体常量、函数 和谓词按照如下规定赋值：和谓词按照如下规定赋值： （1）为每个个体常量指派）为每个个体常量指派D中的一个元素；中

8、的一个元素； （2）为每个）为每个n元函数指派一个从元函数指派一个从Dn到到D的映射，其中的映射，其中 Dn=(x1,x2,xn)|x1,x2,xn D （3）为每个）为每个n元谓词指派一个从元谓词指派一个从Dn到到F,T的映射；的映射； 则称这些指派为公式则称这些指派为公式P在在D上的一个解释。上的一个解释。 n永真：永真： n如果谓词公式如果谓词公式P，对个体域，对个体域D上的任何一个上的任何一个 解释都取得真值解释都取得真值T，则称，则称P在在D上是永真的。上是永真的。 n如果如果P在每个非空个体域上均永真，则称在每个非空个体域上均永真，则称P 永真。永真。 n永假（不可满足性）永假（不

9、可满足性） n如果谓词公式如果谓词公式P对于个体域对于个体域D上的所有解释上的所有解释 都取得假值都取得假值F，则称，则称P在在D上是永假的；上是永假的； n如果如果P在每个非空个体域上均永假，则称在每个非空个体域上均永假，则称P 永假。永假。 n可满足的：可满足的： n对于谓词公式对于谓词公式P，如果至少存在一个解释使，如果至少存在一个解释使 得公式得公式P在此解释下的真值为在此解释下的真值为T，则称公式，则称公式P 是可满足的。是可满足的。 n不可满足的：不可满足的： n对谓词公式对谓词公式P，如果不存在任何解释，使得，如果不存在任何解释，使得 P的取值为的取值为T，则称公式，则称公式P是

10、不可满足的。是不可满足的。 4.2 推理相关知识推理相关知识 n推理：推理： 指从已知事实出发，运用已掌握的知识，推导指从已知事实出发，运用已掌握的知识，推导 出其中蕴含的事实性结论或归纳出某些新的出其中蕴含的事实性结论或归纳出某些新的 结论的过程。结论的过程。 n推理分类：推理分类： n自然演绎：已知事实自然演绎：已知事实 推理规则推理规则 结论结论 n归结：否定结论归结：否定结论 前提条件前提条件 矛盾矛盾 nSkolem化化： 公式形式是很多样的。这就会给机器的形式化公式形式是很多样的。这就会给机器的形式化 处理带来很大的麻烦。为了便于机器处理，把处理带来很大的麻烦。为了便于机器处理，把

11、 公式化成统一的标准形式，即公式化成统一的标准形式，即SKOLEM标准标准 型。型。 nSkolem标准型：标准型： 设设P是公式，是公式，P等价于等价于 x1 xnG(x1. xn)，并且，并且 GG1 Gm，其中，其中G1,Gm都是子句，则称都是子句，则称 G的子句集的子句集 S = G1,Gm 为公式为公式P的的Skolem标准型。标准型。 n对公式对公式P的的SKOLEM化的步骤如下：化的步骤如下： （1）将）将P化为前束范式化为前束范式 （Q1x1）（Qnxn）H(x1. xn) 其中其中 Q1Qn是存在量词或者全称量词，是存在量词或者全称量词，H为合为合 取范式的形式取范式的形式,

12、不含不含, ； （2）用如下方法消去存在量词：）用如下方法消去存在量词： i) 若若Qi是一个存在量词，并且它的左边没是一个存在量词，并且它的左边没 有全称量词，则用一个有全称量词，则用一个H中没有的常量符中没有的常量符 号代替号代替H中所有的中所有的xi，之后消去（之后消去（Qixi） ii) 若若Qi是一个存在量词，并且是一个存在量词，并且Qj1,Qjk是是 Qi左边的全称量词，则取一个左边的全称量词，则取一个H中没有的中没有的 函数函数k元符号元符号f, 用用f(xj1,xjk)代替代替xi,之后之后 消去（消去（Qixi）。 n公式公式P经过如上处理，可以化为经过如上处理，可以化为 x

13、1 xn(G1 Gm) 的形式，其中的形式，其中G1,Gm都是子句。省略全都是子句。省略全 称量词，再用称量词，再用“，”取代合取符号，便得取代合取符号，便得 到公式到公式P的的Skolem标准型标准型G1,Gm 。 n任意公式都有与之相对的子句集。任意公式都有与之相对的子句集。 n一个公式与它的一个公式与它的Skolem标准型未必等值，标准型未必等值， 但在不可满足的意义上是一致的。但在不可满足的意义上是一致的。 n置换置换：是形如：是形如t1/x1, tn/xn的一个有限集合。的一个有限集合。 其中其中xi（i=1,n） 是两两不同的变量符号是两两不同的变量符号, ti是是 不同于不同于x

14、i的项。的项。 n置换作用于表达式置换作用于表达式： 给定置换给定置换 =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 置换满足结合

15、律置换满足结合律 n ( ) = ( ) n 置换不满足交换律置换不满足交换律 n n = = 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，

16、则，则 E1 =g(a, f(z)=E2 ，所以，所以 也是也是E1与与E2的的 合一合一置置换。换。 显然显然 比比 简单，易证简单，易证 = ，其中，其中 =h(u)/z n 最一般合一置换求法最一般合一置换求法： n设有公式：设有公式：E1=P(x,y,z); E2= P(x,f(a),g(b) n从左至右查找不同的项，构成了不一致集：从左至右查找不同的项，构成了不一致集： D1=y,f(a) n继续向右比较又得到一个不一致集：继续向右比较又得到一个不一致集： D2=z,g(b) n置换为置换为 = f(a)/y, g(b)/z n 求一般置换算法：令求一般置换算法：令W= E1,E2

17、n令令 k=0,Wk=W,k=;是空置换是空置换, 表示不作置换。表示不作置换。 n如果如果Wk只有一个表达式，则算法停止，只有一个表达式，则算法停止，k就是所要求的就是所要求的 结果结果. n找出找出Wk的不一致集的不一致集Dk 。 n若若Dk中存在元素中存在元素xk和和tk ，其中，其中xk是变元，是变元，tk是项，且是项，且xk不不 在在tk中出现，则：中出现，则： k+1=k tk/xk n Wk+1=wktk/xk k=k+1 然后转（然后转（2）。）。 n算法终止，算法终止，W的一般合一置换不存在。的一般合一置换不存在。 n可以证明，如果可以证明，如果E1和和E2可合一，则算法必停

18、可合一，则算法必停 止于第止于第2步步。 4.2 Horn逻辑程序逻辑程序 n人工智能人工智能： n 知识库：用于推理的知识知识库：用于推理的知识 n 数据库：事实和论据数据库：事实和论据 n 推理：对知识和数据的消解，获得结论推理：对知识和数据的消解，获得结论 4.2 Horn逻辑程序逻辑程序 n已知的知识表示方法有已知的知识表示方法有 n产生式表示法产生式表示法 n语义网络表示法语义网络表示法 n逻辑表示法逻辑表示法 n产生式表示法是一类很重要的方法，知识表示产生式表示法是一类很重要的方法，知识表示 成成IF THEN 的形式。采用产生式方法，的形式。采用产生式方法， 可以将规则与事实以统

19、一的格式表示，即可以将规则与事实以统一的格式表示，即Horn 子句。子句。 4.2 Horn逻辑程序逻辑程序 n如果在一个子句中最多含有一个正文字，如果在一个子句中最多含有一个正文字， 那么该子句称为那么该子句称为Horn子句子句。 n若一个子句集内的子句个数有限且都是若一个子句集内的子句个数有限且都是 Horn子句，那么该子句集称为一个子句，那么该子句集称为一个Horn 逻辑程序逻辑程序。 4.2 Horn逻辑程序逻辑程序 nHorn子句可以表示成如下形式：子句可以表示成如下形式： 规则体规则体规则头规则头 其中规则体一般是其中规则体一般是n个原子的合取，个原子的合取， n=0,1,。规则头

20、可以是单个原子，也可。规则头可以是单个原子，也可 以是空。以是空。 4.2 Horn逻辑程序逻辑程序 n规则规则：规则体非空且规则头非空的子句。例如，：规则体非空且规则头非空的子句。例如， father(z, y), father(y, x)grandfather(z, x) n事实事实：规则体空且规则头非空的子句。例如，：规则体空且规则头非空的子句。例如， father(John, Peter)。 n目 标目 标 ： 无 规 则 头 的 子 句 ， 例 如 ，： 无 规 则 头 的 子 句 ， 例 如 ， grandfather(Smith, Peter)，即要查询，即要查询Smith是是

21、否是否是Peter的祖父？的祖父？ 4.2 Horn逻辑程序逻辑程序 n一个一个Horn逻辑程序是逻辑程序是Horn子句的集合，也就是子句的集合，也就是 规则和事实的集合。因此，一个规则和事实的集合。因此，一个Horn逻辑程序逻辑程序 相当于一个知识库。相当于一个知识库。 n推理即是通过对一组子句按照一定的方式进行推理即是通过对一组子句按照一定的方式进行 消解最终得到新的公式。消解最终得到新的公式。 n自动推理的过程即给定目标子句，机器自动推理的过程即给定目标子句，机器 按照一定的顺序对逻辑程序中的子句进按照一定的顺序对逻辑程序中的子句进 行消解，最后得到目标子句，或者得出行消解，最后得到目标

22、子句，或者得出 目标不可满足的结论。目标不可满足的结论。 n命题命题Horn逻辑的自动推理逻辑的自动推理 n谓词谓词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

23、基于上述消解方式，求证一个目标基于上述消解方式，求证一个目标 S：A1,An 需要逐一以需要逐一以S的体中的每一个原子的体中的每一个原子Ai作为新的目作为新的目 标进行求证。标进行求证。 A1,An 也称为也称为S的子目标。的子目标。 n在以一个原子在以一个原子Ai为目标进行求证时，考察子句为目标进行求证时，考察子句 集内所有头部是集内所有头部是Ai的子句，以此子句的体作为的子句，以此子句的体作为 新的目标。新的目标。 4.3 命题命题Horn逻辑中的自动推理逻辑中的自动推理 n当某个关于当某个关于A的子句体部的所有原子得到满足的子句体部的所有原子得到满足 时，直接返回时，直接返回A是正确的，

24、而不用再接着考察是正确的，而不用再接着考察 头是头是A的其他子句。的其他子句。 n当对于某个原子当对于某个原子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是是 事实事实 el

25、se if ( TorF(A1)= = TorF(Am)=1) /A1 Am 是第是第i条规则体内的所有原子条规则体内的所有原子 then return 1; /由由i规则推出原子规则推出原子A的正确的正确 i=i+1; /第第i条规则体内并非所有原子正确，从而需条规则体内并非所有原子正确，从而需 要考察别的规则要考察别的规则 return 0; /考察了所有的规则，都不能推出考察了所有的规则，都不能推出A 4.4 谓词谓词Horn逻辑中的自动推理逻辑中的自动推理 n谓词谓词Horn逻辑的消解要复杂一些。消解方式如逻辑的消解要复杂一些。消解方式如 下。若有子句下。若有子句 S1：A1,An S

26、2：B1,BmB， 并且并且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 谓词谓词Hor

27、n逻辑中的自动推理逻辑中的自动推理 n在以一个原子在以一个原子Ai为目标进行考察时，考为目标进行考察时，考 察每一个头部是察每一个头部是Ai的子句，以此子句的的子句，以此子句的 体作为新的目标。返回的不是体作为新的目标。返回的不是0（假）或（假）或 者者1（真），而应是一个置换的集合（真），而应是一个置换的集合。 n为此先要给出置换算法为此先要给出置换算法Substitution以及以及 求表达式合一算法求表达式合一算法Unify。 4.4 谓词谓词Horn逻辑中的自动推理逻辑中的自动推理 将置换将置换 作用于表达式作用于表达式e的算法如下的算法如下 Substitution(e, ) if

28、(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

29、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

30、; 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)，即查

31、询，即查询Smith 是否是是否是Peter的祖父？的祖父？ 4.4 谓词谓词Horn逻辑中的自动推理逻辑中的自动推理 推理过程如下；推理过程如下； 1. 首先通过合一置换首先通过合一置换 =Peter/x, Smith/z，将目标，将目标 与知识库中第一条规则的规则头匹配，得到新与知识库中第一条规则的规则头匹配，得到新 目标目标 father(Smith, y), father(y, Peter) 2. 考察知识库中第二条和第三条规则，通过合一考察知识库中第二条和第三条规则，通过合一 置换置换 =John/y与知识库中的事实匹配与知识库中的事实匹配 father(Smith, John),

32、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=i11; 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 ; Prolog nProlog(Programming in logic)语言是以语言是以Horn子句子句 逻辑为基础的高级程序设计语言。逻辑为基础的高级程序设计语言。 n1972年，法国马赛大学的年，法国马赛大学的Alain. Colmerauer提出提出 了了Prolog的雏型。的雏型。 n1975年，年，Prolog被用于问题求