导读:本文包含了自动定理证明器论文开题报告文献综述及选题提纲参考文献，主要关键词:形式验证,形状图逻辑,结构归纳,自动定理证明
自动定理证明器论文文献综述
郝爔[1]（2015）在《解决自动定理证明器在程序验证中两点能力不足的办法》一文中研究指出当今社会,计算机安全问题的严峻形势使得人们迫切需要高可信软件。形式化验证方法是提高软件可信度的一种可靠的方法,其中基于演绎推理的的方法更是近些年来的研究热点。本实验室基于演绎推理方法设计并实现了一种形式化程序验证的工具——面向PointerC的程序验证原型系统(简称原型系统)。它是一个源码级的程序验证工具,其特色是先通过形状分析得到指针之间的关系,然后根据Hoare逻辑的扩展对程序进行演绎推理并生成验证条件,最后交给自动定理证明器证明。然而自动定理证明器对于本原型系统来说具有两点能力不足,第一点是无法进行归纳证明,第二点是无法自动发现全称量词彼此之间的联系。本文针对这两个问题,在实验室原有的工作基础上对原型系统的功能进行改进。本文的主要贡献如下：第一,设计并实现对程序员提供的性质定理的自动归纳证明。为了提高断言语言的表达能力,原型系统引入自定义归纳谓词。程序员有时在编写程序代码的过程中,会利用到递归定义谓词的归纳性质。同时,由于自动定理证明器在证明验证条件的过程中无法推导出这些归纳性质,程序员需要给出相关的性质定理辅助自动定理证明器证明。为了保证性质定理的正确性,本文给出了对性质定理先进行分析后进行结构归纳的方法,实现了性质定理的自动证明。第二,改进了带有全称量词断言的程序验证功能。当验证条件中包含全称量词断言时,自动定理证明器会因为无法发现多个全称量词彼此之间的关系而证明失败。本文提供了一种结合形状图对全称量词断言分组的思路,并且依据这种思路对验证条件中出现的全称量词进行处理,从而使得原型系统可以通过验证条件中包含多个全称量词断言的程序的验证。本文对原型系统进行扩展后,解决了当前原型系统中因为自动定理证明器两点能力不足带来的问题。保证了程序员提供的性质定理的正确性,不仅使得之前所有操作易变数据结构的程序实例的验证结果更加可靠,还使得原型系统可以验证包含多个全称量词断言的程序。(本文来源于《中国科学技术大学》期刊2015-04-22）
王振明,陈意云,王志芳[2]（2010）在《一个用于指针程序验证的自动定理证明器的设计与实现》一文中研究指出对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.(本文来源于《小型微型计算机系统》期刊2010年05期）
王振明,陈意云,王志芳[3]（2009）在《用于指针逻辑的自动定理证明器(英文)》一文中研究指出提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL的工具中得以实现.APL自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自动定理证明器.(本文来源于《软件学报》期刊2009年08期）
王振明[4]（2009）在《用于指针逻辑的自动定理证明器的设计与实现》一文中研究指出对高可信软件需求的增加使得指针程序的验证成为近十几年的研究热点,自动定理证明作为形式化方法之一,在软件验证和程序分析工具当中发挥着及其重要的作用。然而,自动定理证明本身是一个非常难于解决的问题,尤其是待解决的问题中存在着指针以及涉及到指针的递归定义的谓词的情况下。考虑到以上问题,我们在一个出具证明编译器框架中设计并实现了一个自动定理证明器和一个起辅助作用的证明检查器,来帮助完成指针程序的验证。实验结果证明,我们的实现不但具有创新性而且具有实际可行性。在本文中,我们首先介绍了项目的研究背景和理论基础,然后提出了一种为指针逻辑来设计自动定理证明器的新技术,这项技术主要是基于变换和替代,我们已经在一个被称为APL的工具中实现了该技术。指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析。此外,本文还介绍了APL自动定理证明器的详细设计和实现,描述了一些关键算法,比如指针逻辑决策过程,整型线性算术决策过程,证明检查算法等等。APL定理证明器是完全自动的,并且APL所产生的证明可以被有效的记录和检查。在出具证明编译器PLCC 2中,我们调用了APL自动定理证明器,并对一些具有代表性的程序进行了测试。实验结果表明,APL完全可以自动地证明使用类C语言编写的关于单链表,双链表和二叉树的指针程序。本文的主要特色和贡献为:1.提出了一种为指针逻辑设计自动定理证明器的新方法。该方法是为了解决基于指针信息集合表示的验证条件的证明问题而设计的。在实现时我们使用了替代,变换,指针分析等基本技术,在指针信息集合上完成各种推理和证明。并且我们使用这种方法为指针逻辑实现了一个完全自动的定理证明器。这在已存在的比较流行的定理证明器中是不曾实现过的。2.设计了指针逻辑的断言语言和相应的断言演算。该断言语言能够以简洁易懂的形式描述指针逻辑的最显着的特点,主要使用指针信息集合的形式表示待验证的指针程序在各程序点上的状态。断言语言和断言演算是定理证明器和证明检查器设计和实现的基础。3.设计了一个证明检查算法,并在一个证明检查器中实现了该算法。该算法不同于已有的证明检查算法之处在于,它主要是使用模式匹配的方法对以指针信息集合表示为主的证明进行快速有效的检查,来保证证明的正确性。4.实现了一个用于指针逻辑的自动定理证明器。该实现主要包含指针逻辑和整型线性算术两大理论的决策过程,独创的验证条件检查器,证明生成、保存和检查模块等。可以完全自动地证明出具证明编译器PLCC所产生的关于单链表,双链表和二叉树等程序实例的验证条件。APL自动定理证明器的实现,使得出具证明编译器PLCC 2不再需要依赖交互式证明工具Coq,能证明更多的、规模更大的程序实例,整个工具的功能因此变得更加强大。(本文来源于《中国科学技术大学》期刊2009-04-12）
张东摩,朱梧槚[5]（1994）在《中介自动推理的理论与实现(Ⅲ)——中介逻辑定理证明器》一文中研究指出文[1]、[2]建立了中介逻辑的表推演理论,本文着重介绍以这一理论为基础设计的实验性中介逻辑定理证明器(MTP)。这一定理证明器能实现中介逻辑各子系统(包括经典一阶逻辑)中定理的自动证明。文中介绍了MTP采用的基本算法、基本结构及技术途径。(本文来源于《模式识别与人工智能》期刊1994年04期）
自动定理证明器论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
自动定理证明器论文参考文献
[1].郝爔.解决自动定理证明器在程序验证中两点能力不足的办法[D].中国科学技术大学.2015
[2].王振明,陈意云,王志芳.一个用于指针程序验证的自动定理证明器的设计与实现[J].小型微型计算机系统.2010
[3].王振明,陈意云,王志芳.用于指针逻辑的自动定理证明器(英文)[J].软件学报.2009
[4].王振明.用于指针逻辑的自动定理证明器的设计与实现[D].中国科学技术大学.2009
[5].张东摩,朱梧槚.中介自动推理的理论与实现(Ⅲ)——中介逻辑定理证明器[J].模式识别与人工智能.1994