基于配对方法的自动定理证明

ＰｅｔｅｒＢ．Ａｎｄｒｅｗｓ提出了自动定理证明的配对方法的理论和算法．本文针对该算法的缺点，给出了一个无需回溯的实现算法。

自动定理证明中带有等词的连接法

连接法是一种较新的自动定理证明的方法．该文讨论了带有等词的连接法，给出了形式化的定义，证明了带有等词的逻辑公式是ｅｑ有效的当且仅当它有互补复合例的规范矩阵的定理，并设计了带有等词的连接法的有关算法．

自动定理证明中RUE-NRF单元输入和锁的演绎

本文在RUE-NRF推理规则的基础上,定义了RUE-NRF输入归结、RUE-NRF单元归结及RUE-NRF锁归结的概念,证明了RUE-NRF输入反驳与RUE-NRF单元反驳的关系,以及RUE-NRF锁反驳的完备性。

基于重写技术的自动定理证明

重写技术是处理等式理论的一种有效方法,它已成功地应用到带等词的一阶谓词逻辑中定理的自动证明。本文介绍基于重写的定理证明方法的基本思想,以及几种具体的证明技术,最后将这类方法与经典的归结证明方法加以比较。

基于面向对象的几何定理自动证明系统设计与实现

针对几何定理自动证明的前推法实现方式,结合面向对象编程工具的特点,实现了一个原型系统。该系统结构简单、清晰,可扩展性强,并能产生可读证明过程。实例分析说明了该原型的有效性。

一个用于指针程序验证的自动定理证明器的设计与实现

对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.

用于指针逻辑的自动定理证明器(英文)

提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL的工具中得以实现.APL自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自动定理证明器.

几何定理自动证明的一种数值测试辅助算法

基于数据挖掘中的聚类分析思想提出一种借助数值测试判断几何图形之间关系 ,以简化定理自动证明中搜索过程的新方法 ,该方法已成功地应用于作者参与开发的平面几何教育软件中 ,达到了加速推理引擎的目的。

自动定理证明:十年回顾

本文主要介绍近十年来定理证明器的发展情况,同时讨论了与自动定理证明相关的一些问题。

支持用户自定义谓词的自动定理证明的研究

在先前设计的一个出具证明编译器原型基础上,增加了可用来描述数据结构性质的自定义谓词,对断言语言表达能力方面做了提升.在出具证明编译器的框架内,借助自动定理证明技术,针对自定义谓词的特点,设计了专门的推理规则,由此实现自定义谓词专用的自动定理证明器原型,并将它并入系统原来的自动定理证明器中.该原型可以用来证明操作单链表、二叉树等共享数据结构的程序的性质,其程序规范中可以使用自定义谓词描述数据有序性、链表长度等性质.

自动定理证明中的一个通用证明法

在自动定理证明中，我们发现一个卓有成效的证明方法——多余文字参数法．利用这一方法可以简单便捷地证明许多难以证明的各种推理策略中的完备性问题．本文列举了如何应用这一方法来证明自动定理证明中归结原理的完备性、语义归结的完备性、线性归结的完备性以及输入归结和单位归结的等价性问题．事实表明这些原本都是十分棘手的证明问题，由于使用了这一方法而变为十分简单而自然的工作。

一个用于一阶逻辑自动定理证明的新算法

本文提出一个用于一阶逻辑(FOPC)自动定理证明的并行算法,它基于分治的思想,把原问题子句集S划分成两个独立的子句集S1和S2,并通过并行地证明S_1和S_2的不可满足性。本文首先讨论了子句集的划分问题,引入了导出子句集及划分因子的概念;然后,在此基础上,提出了FOPC定理证明的并行算法;最后,给出了算法的有效性和完备性证明。文中还讨论了子句集的化简及算法性能评价等问题。

命题逻辑定理自动证明的直证式消解原理

消解算法对命题逻辑定理自动证明是普遍能行的,但现行消解证明只能归属于反证法。本文提出直证式消解原理,从析取范式能否消解出最简恒真式来判定和证明定理。其消解规则是原消解规则的对偶定理,消解过程中每步得式也都是原消解过程相应得式的否定式。只须赋予新的逻辑涵义,消解的集合表达形式仍可使用。直证式消解算法也具有可靠性、完全性、能行性,然而剔除了反证步骤,更简明直接。

定理证明自动化的实现

在计算机上实现逻辑推理和定理证明的自动化,是人们探索很久的问题。本文从基本概念出发,较系统地分析了定理证明自动化的实现问题,并通过实例说明定理证明自动化的实现过程。

在APPLEⅡ机上实现自动定理证明

作者根据锁归结(lock resolution)原理用LISP语言编制了完整的框图和程序,并在APPLE Ⅱ机器上实现了对命题逻辑中的定理的证明。归结原理的证明过程采用了反驳(refutation)的形式,这很像数学中的反证法。为了使一个定理能在计算机上得以证明,首先要把定理的前提和结论都化为逻辑表达式。

运用定理证明器ACL2验证机器人操作系统ROS节点间通信

作为一种开源的机器人操作系统,ROS在家用或服务性机器人上也得到广泛应用,保证其设计的正确性相当重要.本文通过定理证明的方法对ROS的节点间通信进行形式化建模与属性验证.对通信层的节点间连接建立和消息传递过程进行抽象建模,模型融合网络拓扑、主题匹配和路由机制等部分,定义函数对其进行描述,提取路由函数的存在性、可达性及正确性等3个关键属性,运用定理证明工具ACL2对ROS节点间通信的功能正确性进行自动验证,证明消息从源节点出发并选择有效的传输路径到达目的节点.这种满足属性要求的参数化模型具有一般性和易扩展性,并能保证ROS节点间通信的终止属性和功能正确性,可为ROS通信层设计的正确性验证工作提供一个有效的方法参考.

形状图理论的定理证明

验证操作易变数据结构的指针程序仍面临很多挑战.数据结构中严重的指针别名显著地复杂化对操作这些结构的程序的推理.为分析和验证操作易变数据结构的指针程序,文中提出了形状图逻辑.形状图是描述程序中静态声明的堆指针变量和动态分配的结构体中指针域变量的指向的一种有向图,能准确表达指针的有效性和指针之间的相等性,可用于判断两个访问表达式是否是别名.形状图逻辑是Hoare逻辑的一种扩展,是一种直接将形状图作为程序中指针断言集的程序逻辑.该文研究形状图的等价理论和蕴含理论以及它们的判定方法和应用.首先,把形状图及其等价规则和蕴含规则分别类比为代数项及其等式规则和重写规则,像研究代数规范的理论那样来研究形状图理论.该文定义了形状图的语法理论和语义理论,定义了形状图重写系统及其终止性、局部合流性和合流性,然后得到基于形状图重写的形状图等价判定和蕴含判定的方法.其次,提出循环不变形状图和递归函数前后形状图的自动推断方法.借助形状图理论的判定方法,该文把一个基于抽象解释的推断循环不变式的一般方法改编成推断循环不变形状图的方法.由于计算终止的递归函数总有非递归的出口,可以先通过非递归路径得到函数的后形状图的初值,然后再在递归路径上迭代求解.从而,可以像推断循环不变形状图那样来推断递归函数的前后形状图.第三,参照Nelson-Oppen框架,提出形状图理论和整数理论组合的一种判定方法.对易变数据结构,除了关心数据结构各节点是否连成预定的形状外,往往还关心数据在这些节点间的排列等特性,它们不能脱离易变数据结构的形状特征而单独验证.为此,所提出的组合判定方法针对这类程序的验证条件的特点,利用程序分析阶段得到的形状图对验证条件的前件中的符号断言按形状图的节点分组;然后运用整数理论为各节点推导出尽可能多的性质;最后才交由定理证明器Z3去自动验证.这种方式有效地避免验证条件证明过程的不终止.基于形状图逻辑以及文中的工作,我们所开发的程序验证系统原型减轻了自动定理证明器的负担,并且能验证易变数据结构上较为复杂的程序,如有序循环双向链表、二叉排序树、伸展树、树堆、二叉平衡树和AA树的插入和删除函数.

机器定理证明的反向归约方法

基于代数和递归函数理论，本文定义了代数递归谓词．代数递归谓词是一类广泛的谓词．基于数学归纳法，作者给出了证明代数递归谓词永真性的反向归约方法及相应的算法Ｒｅｄｕｃｔｉｏｎ．由于采用反向归约方式来完成定理证明，从根本上消除了正向组合式定理证明所产生的组合爆炸，因而极大地提高了定理证明的效率．

COMPS连接法定理证明系统

连接法是继归结法以后由Bibel W等人于80年代初提出的一种自动定量证明的方法.本文介绍了一个以PASCAL语言在IBM4361中型机上实现的COMPS连接法定理证明系统.＊