问题求解的基本方法-基于归结的演绎推理.ppt

上传人:龙*** 文档编号:1043387 上传时间:2018-11-24 格式:PPT 页数:53 大小:624.50KB
下载 相关 举报
问题求解的基本方法-基于归结的演绎推理.ppt_第1页
第1页 / 共53页
问题求解的基本方法-基于归结的演绎推理.ppt_第2页
第2页 / 共53页
问题求解的基本方法-基于归结的演绎推理.ppt_第3页
第3页 / 共53页
问题求解的基本方法-基于归结的演绎推理.ppt_第4页
第4页 / 共53页
问题求解的基本方法-基于归结的演绎推理.ppt_第5页
第5页 / 共53页
点击查看更多>>
资源描述

1、问题求解的基本方法-基于归结的演绎推理 2复习 合适公式 合取 范式 合适公式的可满足性 3合适公式的定义 1) 单一谓词公式(即原子公式)是合适公式;2) 若 A是合适公式,则 A也都是合适公式;3) 若 A和 B都是合适公式,则 A B、 A B、 A B和A B也都是合适公式;4)若 A是合适公式, x是约束变量,则( x) A和( $x)A也是合适公式5)只有按上述规则( 1)至( 4)求得的公式,才是合适公式 4 合取范式和析取范式定义 1:文字是原子公式或原子公式之非定义 2:公式 G称为合取范式 ,当且仅当 G有形式G1 Gn(n=1),其中每个 Gi都是文字的析取式定义 3:公

2、式 G称为析取范式 ,当且仅当 G有形式G1 Gn(n=1),其中每个 Gi都是文字的合取式 5合适公式的永真性和可满足性1) 合适公式的永真性 若某合适公式 P对于某论域 D上的所有可能的解释都有真值 T,则称 P在 D上是永真的;若 P在每个可能的非空论域上均永真,则称 P是永真的。2) 合适公式的可满足性对于合适公式 P,若在论域 D上至少可以建立一个解释,使 P有真值 T,则称 P在 D上是可满足的;若至少有一个论域使 P可满足,则称 P是可满足的。 6一 归结演绎方法 F1, F2, ,F n|= W F1 F2 Fn = W证明的方法可分二大类 :直接证明 F1 F2 Fn = W

3、 为永真 , 即演绎法 间接证明 (F1F 2 F n = W)为永假,即反证法 反证法:F1 F2 Fn W证明上式永假,这实际上就是要证明 F1, F2, ,Fn W 是一个矛盾集 7概念: 文字:谓词公式或其取反P( a,b), Human(x), 父亲( a,A) 子句:一些文字的析取(谓词的和),不含任何文字的子句称为空子句,记为 Q(y,b) R(x) 子句集:所有子句的集合P(a,x,f(x), Q(g(x),b) P(a,x,f(x) Q(g(x),b)P(x,y) P(y,z),Q(x,z) 8子句及子句集的作用:合取范式可以定义为子句的合取进而把合取范式表示为子句集当合适公

4、式 F化简为标准化的子句集 S时,有一个 重要性质 ,即 S的不可满足 (对于任意论域上的任意解释, S中都至少有一个子句真值为 F)成为 F永假的充分必要条件 9 Skolem标准型前束范式中消去所有的量词,这种形式的合适公式称为 Skolem标准型任何一个合适公式都可以转化为与之对应的Skolem标准型,但不唯一前束范式谓词公式 P如果具有以下的形式,即把所有的量词都提到最左端去:( Q1x1)(Q2x2)(Q nxn)P(x1,x2,x n) 10将合适公式 G转换成前束范式; 消去前束范式中的存在量词,略去其中的任意量词,生成 Skolem标准型 将 Skolem标准型中的各个子句提出,表示为集合形式 可以看出 Skolem标准型必须满足合取范式的条件例如: P( a,x,f(x) Q(g(x),b) R(x)的子句集为:P( a,x,f(x) , Q(g(x),b) , R(x) 子句集的求取过程 :

展开阅读全文
相关资源
相关搜索

当前位置:首页 > 教育教学资料库 > 课件讲义

Copyright © 2018-2021 Wenke99.com All rights reserved

工信部备案号浙ICP备20026746号-2  

公安局备案号:浙公网安备33038302330469号

本站为C2C交文档易平台,即用户上传的文档直接卖给下载用户,本站只是网络服务中间平台,所有原创文档下载所得归上传人所有,若您发现上传作品侵犯了您的权利,请立刻联系网站客服并提供证据,平台将在3个工作日内予以改正。