当前位置:高等教育资讯网  >  中国高校课件下载中心  >  大学文库  >  浏览文档

上海交通大学:《人工智能》课程教学资源(PPT课件)第3章 基于谓词逻辑的机器推理(3.2-3.7)

资源类别:文库,文档格式:PPT,文档页数:47,文件大小:267.5KB,团购合买
3.2 归结演绎推理 3.3 应用归结原理求取问题答案 3.4 归结策略 3.6 Horn子句归结与逻辑程序 3.7 非归结演绎推理
点击下载完整版文档(PPT)

第三章基于谓词逻辑的机器推理--32归结 演绎推理 321子句集 定义1原子谓词公式及其否定称为文字;文字的析取式 称为子句;r个文字组成的子句称为r文字子句。1-文 字子句也称为单元子句。不含任何文字的子句称为空 子句,记为或ML。由子句构成的集合称为子句集。 任何一个谓词公式都可以化为子句集,步骤如下: (1)、利用等价式A→B分AVB 和A分>B令(A→>B)∧(B→A)消去联结词“→”和 (2)、缩小否定联结词的作用范围,使其仅作用于 原子公式。可利用下列等价式:

第三章 基于谓词逻辑的机器推理----3.2 归结 演绎推理 3.2.1子句集 定义1 原子谓词公式及其否定称为文字;文字的析取式 称为子句;r个文字组成的子句称为r-文字子句。1-文 字子句也称为单元子句。不含任何文字的子句称为空 子句,记为•或NIL。由子句构成的集合称为子句集。 任何一个谓词公式都可以化为子句集,步骤如下: (1)、利用等价式A → B  A B 和 A  B  (A → B) (B → A)消去联结词“ → ” 和 “  ”。 (2)、缩小否定联结词的作用范围,使其仅作用于 原子公式。可利用下列等价式:

GAbA (AVB)今=A∧=B; (A入B)_AyB; XA(x)彐xA(x); 彐xA(x)分Vx-A(X) (3)、重新命名变元名,使不同量词约束的 变元有不同的名字

  A A; (AB)   A   B; (A  B)  A B; xA(x)  x A(x); xA(x)   x A(x) (3)、重新命名变元名,使不同量词约束的 变元有不同的名字

(4)、消去存在量词。若存在量词不在全称量 词的辖域内,则用一个常量符号替换该存在量 词辖域中的相应约束变元。这样的常量称为 Skolem常量;若该存在量词在一个或多个全称 量词的辖域内,则用这些全称量词指导变元的 个函数替换该存在量词约束的变元。这样的 函数称为 Skolem函数。 例如∨x1Vx2xn3yP(x1x2,xny)中y可用 Skolem函数f ,xn)替换为x1Vx2 VX,P(XI xn, f(x1,x,,.,n)

(4)、消去存在量词。若存在量词不在全称量 词的辖域内,则用一个常量符号替换该存在量 词辖域中的相应约束变元。这样的常量称为 Skolem常量;若该存在量词在一个或多个全称 量词的辖域内,则用这些全称量词指导变元的 一个函数替换该存在量词约束的变元。这样的 函数称为Skolem函数。 例如x1 x2 • • •xnyP(x1 ,x2 ,…, xn ,y)中y可用 Skolem函数f(x1 ,x2 ,…, xn )替换为x1 x2 • • • xnP(x1 ,x2 ,…, xn ,f(x1 ,x2 ,…, xn ))

(5)、把全称量词全部移到公式的左边 (6)、把全称量词后面的公式利用等价关系 Av(BAC)分(AVB)∧(AVC)化为子句的合取 式,得到的公式称为 Skolem标准形。 Skolem 标准形的一般形式为Vx1Yx2xnM,其中 M是子句的合取式。 (7)、消去全称量词。 (8)、对变元更名,使子句间无同名变元

(5)、把全称量词全部移到公式的左边。 (6)、把全称量词后面的公式利用等价关系 A(B C)  (AB) (A C)化为子句的合取 式,得到的公式称为Skolem标准形。Skolem 标准形的一般形式为x1 x2 • • •xnM,其中 M是子句的合取式。 (7)、消去全称量词。 (8)、对变元更名,使子句间无同名变元

(9)、消去合取词入,以子句为元素组成的 集合称为谓词公式的子句集 例、把谓词公式∨x{yP(xy)→> √yQ(xy))R(xy)化为子句集。 定理1谓词公式G不可满足当且仅当其子句 集S不可满足。子句集S是不可满足的是指其 全部子句的合取式是不可满足的

(9)、消去合取词 ,以子句为元素组成的 集合称为谓词公式的子句集。 例、把谓词公式x{yP(x,y) → y[Q(x,y)→R(x,y)]}化为子句集。 定理1 谓词公式G 不可满足当且仅当其子句 集S不可满足。子句集S是不可满足的是指其 全部子句的合取式是不可满足的

3.2.2命题逻辑中的归结原理 ◆要证明在前提P下结论Q成立,即是证明P→Q永真, 这只须证明P∧_Q不可满足。根据定理1,只须证 明P∧Q的子句集不可满足。由于子句之间是合取 关系,只要有一个子句不可满足,则整个子句集不 可满足。由于空子句是不可满足的,所以如果子句一 集中包含空子句,则该子句集是不可满足的。若子 句集中不包含空子句,则可通过 Robinson提出的归 结原理对子句集进行归结,归结过程保证子句集的 不可满足性不变。一旦归结出空子句,则证明结束 因此,归结原理把定理的证明化为子句集中归结出 空子句的过程

3.2.2 命题逻辑中的归结原理 要证明在前提P下结论Q成立,即是证明P → Q永真, 这只须证明P  Q不可满足。根据定理1,只须证 明P  Q的子句集不可满足。由于子句之间是合取 关系,只要有一个子句不可满足,则整个子句集不 可满足。由于空子句是不可满足的,所以如果子句 集中包含空子句,则该子句集是不可满足的。若子 句集中不包含空子句,则可通过Robinson提出的归 结原理对子句集进行归结,归结过程保证子句集的 不可满足性不变。一旦归结出空子句,则证明结束。 因此,归结原理把定理的证明化为子句集中归结出 空子句的过程

定义4、设L是一个文字,则称L与为互补 文字。 定义5、设C1、C2是命题逻辑中的两个子句, C1中有文字L1,C2中有文字L2,且L1与L2 互补,从C1,C2中分别删除L1,L2,再将剩 余部分析取起来,构成的新子句C12称为C1与 C2的归结式(消解式),C1,C2称为C12的亲 本子句

定义4、设L是一个文字,则称L与L为互补 文字。 定义5、设C1、C2是命题逻辑中的两个子句, C1 中有文字L1 , C2 中有文字L2,且L1与L2 互补, 从C1,C2中分别删除L1 , L2,再将剩 余部分析取起来,构成的新子句C12称为C1与 C2的归结式(消解式), C1,C2称为C12的亲 本子句

定理2、归结式C12是其亲本子句C1与C2 的逻辑结论 ※推论、设C1,C2是子句集S的两个子句, C12是它们的归结式,则 (1)若用C12代替C1和C2后得到新子 句集S1,则由S1的不可满足性可推出原 子句集S的不可满足性。即 S1不可满足→S不可满足

定理2、归结式C12是其亲本子句C1与C2 的逻辑结论。 推论、设C1,C2是子句集S的两个子句, C12是它们的归结式,则 (1)若用C12代替C1和C2后得到新子 句集S1,则由S1的不可满足性可推出原 子句集S的不可满足性。即 S1不可满足S不可满足

(2)若把C12加入到S中,得到新子句集 S2,则S2与S在不可满足意义上是等价 的。即 S2不可满足◇S不可满足 例、用归结原理证明R是P,(P∧Q) →R,(SVU)→R,U的逻辑结 果

(2)若把C12加入到S中,得到新子句集 S2,则S2与S在不可满足意义上是等价 的。即 S2不可满足 S不可满足 例、用归结原理证明R是P, (P  Q) → R, ( SU) → R,U的逻辑结 果

3.2.3替换与合 定义6、一个替换( Substitution是形如{t1/x1 t2/x2…,n/xn}的有限集合,其中t,t2,…,tn 是项,x1,x2,,xn是互不相同的个体变元。 七/x表示用t代换x1。t与x不同,x也不能出 现在中(=1,2,n 例、(ax,g(y)y,fg(b)/z}是一个替换, g(y)x,fx)y}不是一个替换

3.2.3 替换与合一 定义6、一个替换(Substitution)是形如{t1 / x1 , t2 / x2 ,…,tn / xn }的有限集合,其中t1 , t2 ,…,tn 是项, x1 , x2 ,…,xn是互不相同的个体变元。 t i / xi表示用t i代换xi 。 t i与xi不同,xi也不能出 现在t j中(j=1,2,…,n)。 例、{a/x, g(y)/y, f(g(b))/z}是一个替换, {g(y)/x, f(x)/y}不是一个替换

点击下载完整版文档(PPT)VIP每日下载上限内不扣除下载券和下载次数;
按次数下载不扣除下载券;
24小时内重复下载只扣除一次;
顺序:VIP每日次数-->可用次数-->下载券;
共47页,可试读16页,点击继续阅读 ↓↓
相关文档

关于我们|帮助中心|下载说明|相关软件|意见反馈|联系我们

Copyright © 2008-现在 cucdc.com 高等教育资讯网 版权所有