人工智能导论ppt课件_第1页
人工智能导论ppt课件_第2页
人工智能导论ppt课件_第3页
人工智能导论ppt课件_第4页
人工智能导论ppt课件_第5页
已阅读5页，还剩11页未读， 继续免费阅读

下载本文档

版权说明：本文档由用户提供并上传，收益归属内容提供方，若内容存在侵权，请进行举报或认领

文档简介

.,3-4归结演绎推理,在人工智能中，几乎所有问题都可以转化为一个定理证明问题。即对前提P和结论Q证明PQ永真，从而（PQ）永假（不可满足），也就是PQ永假。海伯伦（Herbrand）理论为自动定理证明奠定了基础（1930）。鲁宾逊（Robinson）归结原理（也称消解原理）使定理证明的机械化成为现实（1965）。吴文俊数学机械化理论（方程组求解）（1977）,.,3-4-1子句集及其化简,子句和子句集原子谓词公式及其否定统称为文字。例：P(x），P(x)，P(f(x),a)任何文字的析取式称为子句。例：P(x)Q(y),P(x,f(x)Q(a,g(x)不包含任何文字的子句称为空子句。空子句是永假的（不可满足），记为或NIL（无，零）由子句或空子句构成的集合称为子句集。例：P(x），P(x)Q(y)，P(x),.,子句集的化简,在谓词逻辑中，任何一个谓词公式都可以通过应用等价关系及推理规则化成相应的子句集。产生谓词公式子句集的算法由下列九步构成：,.,（1）消去连接词“”和“”利用等价关系,.,（2）减少否定符号的辖域利用等价关系,.,（3）变元标准化使不同量词约束的变元名字不同。,.,（4）化为前束范式把所有量词都移到谓词公式的最左边，但不能改变其相对顺序。,.,（5）消去存在量词分两种情况：若存在量词的左边无全称量词，则用一个新的个体常量（不同于已有常量）替换该存在量词约束的变元。,.,若存在量词的左边有全称量词，则用一个新的函数（不同于已有函数）替换该存在量词约束的变元，该函数的变量由出现在该存在量词左边的全称量词约束的变量构成，具体形式不限（实际上只是一种形式而已）。,.,（6）消去全称量词消去全称量词，得到一个谓词公式，其中变元是被全称量词约束的。,.,（7）化为合取范式（子句的合取）利用等价关系式的分配律化为合取范式。,.,（8）将合取范式的所有子句构成子句集,.,（9）变换子句变元名，使构成子句集的任意两个子句的变元名不同。,.,作业,p.1003-11,.,子句集的应用,谓词公式是不可满足的（永假）当且仅当该谓词公式产生的子句集是不可满足的。要判断一个谓词公式是不可满足的，就要说明该谓词公式在任何非空个体域上永假。这往往是困难的。海伯伦构造了一个特殊的域（称为海伯伦域），并且证明只要对这个特殊域上的一切解释进行判定是否不可满足就可以了。,.,定理3-1设有谓词公式F，其标准子句集为S，则F为不可满足的充要条件是S为不可满足的。参考书美M.D.戴维斯，E.J.威尤克著
人人文库> 全部分类> 教育资料 > 课件下载

温馨提示

  • 1. 本站所有资源如无特殊说明，都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等，如果需要附件，请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸，网页内容里面会有图纸预览，若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对用户上传分享的文档内容本身不做任何修改或编辑，并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容，请与我们联系，我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

最新文档

评论

0/150

提交评论