基于表的定理证明系统

《基于表的定理证明系统》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、原创性声明本人声明:所呈交的硕士学位论文，是本人在指导教师的指导下，独立进行研究工作所取得的成果。除文中己经注明引用的内容外，本论文不包含任何其他个人或集体己经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集体，均已在文中以明确方式标明。本人完全意识到本声明的法律结里}h太人7-k相_学位论文作者签名:均奔务日期:;?-"3年5月/，日关于论文使用授权说明本人同意学校有权保留并向国家有关部门送交学位论文的复印件，允许论文被查阅和借阅·(同氢不同意)学校及国家有关机构有权公布论文的全部或部分内容，并采用影印、缩印或

2、其他复制手段保存论文。论“作者签“:汤料指导教师签名:}btA日期:yoo4.05'.10日期:?w3.Gs-,!o内容提要定理机器证明是许多基于逻辑的推理系统的核心，因此提高自动定理证明系统的效率具有重要的意义，表方法由于其适用于非经典逻辑的推理而受到重视，结合了其它推理方法中的剪枝技术的表方法，在解决一阶逻辑的问题时也显示了很强的优势。本文从实现一个高效的系统出发。对表方法进行了深入细致的分析，设计并实现了基于表方法的一阶定理证明系统。本文首先概述了表方法的发展，详细分析，了用于连接表方法的各种剪枝技术，井着重给出了本

3、文所实现系统中使用的超表方;法和采用superposition方法的超表方法。本文还介绍了基于表方法的定理证明系统的丧计与实现，并以TPTP问题库中的问题对系统进行了测试。铡试结果表明该系.统能够在给定的时间内证明大部分输入公式的不可满足性，该系统和一些著名的ATP系统在速度上的差异表明该系统还需要加强剪枝技术的应用.第一童引言第一章引言1.1研究背景及意义在人工智能应用的许多方面，例如演绎数据库和基于模型的诊断等应用中，其知识表示方法采用的都是基于逻辑的方法，这些应用系统的推理部分都要求能够判断在给定的逻辑框架中，某个结

4、论是否成立。由此，定理机器证明实现效率的提高对于提高这些应用系统的性能具有重要的意义。每年一次的自动演绎会议(CADE)旨在交流在自动演绎的各方面的最新进展，为了促进自动定理证明(ATP)系统的发展，同时亦举行CADE自动定理证明系统竞赛(CASC)来评价正确的、全自动的、经典的一阶逻辑ATP系统。CASC中出现了各种高效的证明系统。例如基于归结方法的。tter，基于表方法的E0.6和E-SETHEOcsp02等.表推理方法由于其推理规则简单.不要求输入的公式一定是合取范式，因而适用于合取范式形式复杂的非经典逻辑，由此受到

5、重视，但用于经典一阶逻辑时却效率不高。将其它推理方法中提高效率的技术引入到子句表中，得到的基于表方法的一阶定理证明器在性能上可以和基于归结方法的一阶定理证明器相媲美。上个世纪九十年代以来，出现了一些高效的基于表方法的定理证明系统，它们有:德国慕尼黑工业大学的DCTP〔非连接方法的表证明器)和SETNEO-,德国卡尔鲁厄大学的3r.W和LEANTAP,前者用于多值逻辑问题，同时可以处理含等词的一阶逻辑问题，后者是用于非经典逻辑的表证明器。1.2本文主要工作本文以研究定理证明中的表方法并加以实现为目标，研究了用于改进表方法的各

6、种剪枝技术，设计实现了基于表方法的一阶定理证明系统。该系统采用面向对象的程序设计方法，采用C++语言实现，实现了对搜索过程的更精确的控制。系统具有灵活的控制性、可移植性、可扩充性等特点。该系统通过实现超表演算来证明一阶逻辑公式的不可满足性，通过采用superposition方法的超表方法来证明含等词的一阶逻辑公式的不可满足性.本文第二章介绍了表方法发展的历史及应用于子句表的各种剪枝技术:第三章详述了系统的两个模块的关键技术:超表演算和superposition方法以及其中用到的广义公式技术;第四章首先给出了基于表方法的定理

7、证明系统的设计，然后讨论了系统实现的相关技术，并用实验测试数据说明了系统的性能指标;最后是结语和工作展望。第二童基于表方法的一阶定理证明第二章基于表方法的一阶定理证明2.1表方法的发展表方法是将所要证明的公式的语法结构和语义结合起来的证明方法，证明过程直观、易于理解.表方法不要求输入的公式一定是合取范式形式，因而适用于合取范式形式复杂的非经典公式的不可满足性证明，这也是表方法受到重视的原因之一。然而，以一般公式形式为输入的表方法用于一阶逻辑公式的证明时，效率和其它证明方法相差很多，后来出现了以合取范式形式为输入的表方法以及

8、一些改进技术，以此为基础的一阶定理证明器在速度上超过了基于归结方法的证明器。2.1.1基本的表方法一阶逻辑公式按照其语法结构可以分为以下四类m0Ba、a:铆X八YA，(xnY)，X，Y，(xVY)，X，YxVYxYx，(X一)Y)X一>Y，xx一Y，，XX￥丫(a)bb(a)(Vx)P(x)P(a)(日