基于Tableau的定理证明器的优化技术研究

发布时间：2017-07-02 17:24

  本文关键词：基于Tableau的定理证明器的优化技术研究，，由笔耕文化传播整理发布。

【摘要】：语义Tableau是一种具有较强直观性和适用性的推理方法.自该方法问世以来,一直吸引着大量人工智能研究者.基于Prolog语言,M.C.Fitting利用语义Tableau方法提出了一种一阶逻辑自动定理证明器.众所周知,系统的实现效率问题一直是人工智能界的一个热点问题.M.C.Fitting给出的定理证明器虽然比较容易理解,但是在具体应用过程中却存在着一定的效率问题,论文便是针对这一问题展开了具体的研究.具体的研究内容如下:1论文首先给出了一阶逻辑语言的项、公式、子句等有关的概念,然后在此基础上研究了一阶逻辑语言理论及其模型系统,并重点探讨了Herbrand模型.2论文介绍语义Tableau方法的理论和实现.首先描述了Tableau方法的概念与其在实际应用过程中的语义Tableau扩展规则,并完成了该方法的可靠性和完备性的证明,重点介绍了在证明完备性过程中所要用到的模型存在定理;其次给出了实现该系统的算法与在Prolog语言下的代码.3通过对M.C.Fitting给出的定理证明器中存在的效率问题进行分析研究,提出了相关的改进,并给出了改进后的算法以及该算法可终止性和正确性的证明.最后进行了相应的对比实验,结果表明:优化后的语义Tableau定理证明器的推理效率得到了显著的提高.
【关键词】：语义Tableau 定理证明器 Prolog
【学位授予单位】：辽宁师范大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：B812.3
【目录】：

• 摘要4-5
• Abstract5-7
• 1 绪论7-9
• 1.1 论文的背景及意义7
• 1.2 论文研究现状7-8
• 1.3 本文的工作8
• 1.4 内容安排8-9
• 2 一阶逻辑基础9-16
• 2.1 一阶逻辑的概念9-10
• 2.2 一阶逻辑的替换10-12
• 2.3 一阶逻辑语义12-14
• 2.4 Herbrand模型14-16
• 3 Tableau方法的理论16-27
• 3.1 一阶逻辑的语义Tableau方法16-17
• 3.2 一阶模型存在定理17-19
• 3.3 一阶语义Tableau的可靠性和完备性19-20
• 3.4 通代20-23
• 3.5 通代的实现23
• 3.6 自由语义Tableau23-24
• 3.7 一阶自由变元Tableau的完备性和可靠性24-27
• 4 一阶自由语义Tableau系统的实现与改进27-33
• 4.1 一阶自由变元Tableau的实现27-28
• 4.2 一阶自由变元Tableau的改进28-30
• 4.3 实验对比30-33
• 结论33-34
• 参考文献34-36
• 附录A 通代实现的代码36-38
• 附录B 一阶自由变元Tableau的实现代码38-43
• 攻读硕士学位期间发表学术论文情况43-44
• 致谢44

【相似文献】

中国博士学位论文全文数据库 前1条

1 江建国;iGeo：智能几何软件的定理证明器[D];中国科学院研究生院（成都计算机应用研究所）;2006年

中国硕士学位论文全文数据库 前6条

1 高华;基于Tableau的定理证明器的优化技术研究[D];辽宁师范大学;2015年

2 郝r;解决自动定理证明器在程序验证中两点能力不足的办法[D];中国科学技术大学;2015年

3 陈波;基于定理证明器HOL的硬件验证研究[D];兰州大学;2006年

4 陈明雁;基于概率检测组合模型的几何定理证明器[D];华东师范大学;2014年

5 程应娥;Isabelle中自动化证明策略的设计与实现[D];兰州大学;2007年

6 游珍;Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用[D];江西师范大学;2009年

  本文关键词：基于Tableau的定理证明器的优化技术研究，由笔耕文化传播整理发布。

本文编号：510855