浅谈机器证明_第1页
浅谈机器证明_第2页
浅谈机器证明_第3页
浅谈机器证明_第4页
浅谈机器证明_第5页
已阅读5页，还剩7页未读， 继续免费阅读

下载本文档

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

文档简介

浅谈机器证明什么是机器证明？提问机器证明是指用计算机程序去自动完成事实的证明，如定理的证明、结论的推理等。要实现机器证明，必须用比较严格的知识表示方法。本节将介绍用归结原理进行定理证明的思路，我们首先了解这种证明方法的知识表示，然后说明归结原理的思想以及如何用它证明问题。1知识的表示在归结原理中，可以使用以下两种形式表示知识：（1）用谓词表示知识，这种方法类似于Prolog语言中知识的表示形式。例1：事实：表示为子句例2：事实：表示为子句例3：事实：表示为子句Mary喜欢打球like(mary,ball)Mary不喜欢打球~like(mary,ball)John很幸运luck(John)（2）通过用符号“Ⅴ”将谓词连接起来的子句表示知识，其中“Ⅴ”表示“或”的意思。例4：事实：表示为子句例5：事实：表示为子句Mary去打球或去看电影play(mary,ball)Ⅴsee(mary,film)Rose不是人，或Rose是会死的人~man(rose)Ⅴdie(rose)2归结原理及其应用简述1965年鲁滨逊提出了归结原理。归结原理的思想是：若子句AⅤBⅤC：及~AⅤD成立，则子句BⅤCⅤD成立。即A和~A可以互相抵消，而得BⅤCⅤD，其中A、B、C、D是谓词或命题。利用归结原理进行定理证明的步骤如下：（1）写出事实的子句集；（2）写出要证明问题的子句；（3）将要证明的问题子句“否定”化，然后将其加入到事实的子句集中；（4）反复用归结原理，对子句集中的子句进行归结（进行消解），并将产生的子句加入到子句集中。若归结得到一个“空子句”，则推理成功，从而定理得证。例6：若下面事实成立：（1）狗不是动物或狗不是麒麟；（2）狗是动物。证明“狗不是麒麟”这一命题为真。证明：第一步，写出事实的子句集：（1）~animal(dog)Ⅴ~kylin(dog)（2）animal(dog)第二步，写出待证结论的子句形式：kylin(dog)第三步，将结论的子句“否定”化后，加入到由事实子句构成的子句集中。（3）kylin(dog)第四步，反复用归结原理，对子句集中的子句进行归结，并将产生的子句加入子句集中。子句（1）和子句（2）进行归结，得：（4）~kylin(dog)子句（3）和子句（4）进行归结，得：（5）NIL（NIL表示空子句）归结得到一个空子句，结论~kylin(dog)成立。例7：若下面事实成立：（1）Rose不是人，或Rose是会死的人；（2）Rose是人。证明“Rose是会死的人”这一命题为真。证明：事子句集：（1）~man(rose)Vdie(rose)（2）~man(rose)将待证结论否定，得：（3）~die(rose)子句（1）和子句（2）进行归结，得：（4）die(

人人文库> 全部分类> 教育资料 > 辅导培训

温馨提示

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

最新文档

评论

0/150

提交评论