AI05-4归结推理.ppt

《AI05-4归结推理.ppt》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第5章知识与推理5.5.1子句集5.5.2命题逻辑的归结原理5.5.3替换与合一5.5.4谓词逻辑的归结原理5.5.5归结策略第5章知识与推理5.5.1子句集谓词逻辑有量词、变量和函数，转换步骤：前束范式Skolem标准形第5章知识与推理子句集文字不含任何连接词的谓词公式原子谓词公式及其否定子句一些文字的析取（谓词的和）空子句不含任何文字的子句/NIL子句集所有子句的集合第5章知识与推理例子子句集{P(a，x，f(x))，Q(g(x)，b)，R(x)}{Q(y，b)R(x)，P(x)}非子句集{P(a，x，y)Q(y，b)，P(x)}{P(x，y)P(y，z)

2、，Q(x,z)}第5章知识与推理例子子句集{P(a，x，f(x))，Q(g(x)，b)，R(x)}{Q(y，b)R(x)，P(x)}非子句集{P(a，x，y)Q(y，b)，P(x)}{P(x，y)P(y，z)，Q(x,z)}第5章知识与推理前束范式如果A中的一切量词都位于该公式的最左边（不含否定词），且这些量词的辖域都延伸到公式的末端(Q1x1)(Q2x2)…(Qnxn)P(x1,x2,…,xn)A是一个前束范式任何谓词公式P的前束范式都是存在的前束范式是不唯一的可利用换名规则和替代规则求前束范式指导变量应互不相同原公式的自由变量在前束范式中还是自由变量原公式的

3、约束变量在前束范式中还是约束变量第5章知识与推理例子(xP(x,y)→yQ(y))→xR(x,y)<=>(xP(x,z)→yQ(y))→xR(x,z)替换原则<=>(xP(x,z)→yQ(y))→tR(t,z)换名原则<=>x(P(x,z)→yQ(y))→tR(t,z)量词辖域收缩与扩张<=>xy(P(x,z)→Q(y))→tR(t,z)量词辖域收缩与扩张<=>xy((P(x,z)→Q(y))→tR(t,z))量词辖域收缩与扩张<=>xyt((P(x,z)→Q(y))→R(t,z))量词辖域收缩与扩张第5章知识与推理Skolem标准形

4、前束范式中消去所有的存在量词任何一个谓词公式都有与之对应的Skolem标准形Skolem标准形不唯一算法依据约束变量换名规则，把公式变型为前束范式依照量词消去原则，消去或略去所有量词Skolem标准型满足合取范式第5章知识与推理量词消去原则消去存在量词“”如果左边没有任何全称量词，则只将其改写成为常量(a,b等)，该常量称为skolem常量如果左边有全称量词，消去时该变量改写成为任意量词的函数(f(x),g(y)等)，该函数称为skolem函数消去全称量词"“简单地省略掉该量词例子(x)(y)P(x，y)可以表示为“每一个人x都有自己的y年龄”，则年龄y与人x有关，可

5、用一个函数f(x)描述这种依赖关系，f(x)把每一个x值映射为存在的y值；(x)(y)P(x，y)(x)P(x，f(x))(y)P(y)P(a)第5章知识与推理定理公式G的Skolem标准形同G并不等值例子谓词公式G=(x)P(x)Skolem标准型为：G=P(a)解释I：个体域D={0,1}常数a=0谓词P(0)=F,P(1)=T在解释I下：G=T，G=F第5章知识与推理例子((x)(y)P(a,x,y)→(x)((y)Q(y,b)→R(x)))=>((x)(y)P(a,x,y))∨(x)((y)Q(y,b)∨R(x)))消去

6、=>(x)(y)P(a,x,y)∧(x)((y)Q(y,b)∨R(x))=>(x)(y)P(a,x,y)∧(x)((y)Q(y,b)∧R(x))缩小否定词作用范围=>(x)(y)P(a,x,y)∧(z)((t)Q(t,b)∧R(z))换名原则=>(x)P(a,x,f(x))∧(z)(Q(g(z),b)∧R(z)))消去原则=>(x)(z)(P(a,x,f(x))∧Q(g(z),b)∧R(z))前束范式=>P(a,x,f(x))∧Q(g(z),b)∧R(z)Skolem第5章知识与推理子句集S求取谓词公式G转换成前束范式消

7、去前束范式中的存在变量，略去其中的任意变量，生成Skolem标准形将Skolem标准形中的各个子句提出，表示为集合形式例子Skolem:{P(a,x,f(x))∧Q(g(x),b)∧R(x)}子句集S：{P(a,x,f(x)),Q(g(x),b),R(x)}第5章知识与推理子句集S求取算法消去蕴含词→和等值词缩小否定词﹁的作用范围，直到其仅作用于原子公式换名/替换原则，使量词不含同名指导变元和约束变元消去存在量词消去所有全称量词化公式为合取范式消去合取词∧，以子句为元素组成集合S第5章知识与推