出具证明编译器中线性整数命题证明的自动生成

近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.     

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

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

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

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

一类构造性几何不等式的机器证明

阐述了一个基于胞腔分解的不等式证明算法．据此算法编制的Maple通用程序能有效地处理含有根式的不等式型定理,对于Bottema等所著《几何不等式》一书中的大部分不等式定理的验证尤其高效．     

几何定理机器证明的强正常升列分解算法

自上个世纪70年代吴文俊的开创性工作以来，几何定理机器证明这个曾被深人研究而停滞不前的分支在自动推理领域变得异常活跃，大量学术论著相继出现。国内外众多学者，如Chou，Koand Hussain，Wangand Gao，Wang，Zhang，Yangand Hou等提出了各种成功的有效的几何定理机器证明算法。这些方法及其变形已由多位学者实施，使用不同的证明器已经获得了大量几何定理的机器证明。这些定理包括(广义)：史坦纳定理；摩勒三分角线定理以及最近确认的泰博猜想。     

Z规格说明中初始状态存在性的证明

Ｚ规格说明中的初始化定量的证明是对基于状态的规格说明的一个标准的检查，本给出了一个证明初始化定理的过程，该过程可自动地构成证明的证据，作为实例，我们该过程证明了两个初始化定理。     

命题时态逻辑定理证明新方法

本文通过对近１０年命题时态逻辑定理证明方法的研究，提出了一种新的证明方法，前人的工作基于对公式的现时部分和后时部分的分解，本文的工作是基于语义反驳树构造。这种新方法为计算机自动证明命题时态逻辑定理，提供了比较好的理论框架．最后还证明了该方法的可靠性和完全性．     

基于串空间的Athena分析技术研究

基于串空间模型的研究是当前安全协议领域的一个研究热点。Song对串空间模型进行了扩展，将模型检验和定理证明结合起来，提出了一种取名为Athena的安全协议分析方法，并基于该方法开发了自动证明工具APV，Song的工作被认为是串空间理论发展的一个重要事件。本文对Athena进行了系统的分析，介绍了Athena的假设条件，给出了Athena的语法和语义，分析了该逻辑的优点和局限性，在此基础上，分析了Athena的核心算法，讨论了Athena算法自动高效的原因，以及该算法如何避免状态空间爆炸的技术，指出了该算法的缺陷，形成原因以及解决的一般方法。最后对Athena方法的发展方向进行了讨论。     

基于向量的几何可读自动证明

几何定理机器证明已经成功发展了多种新方法,但其中对中学几何中向量的机器证明研究没有抓住其回路的基本特征.文中以向量的回路为出发点,提出了基于回路的向量可读证明新方法,开发了机器证明新程序.该程序对常见的构造类型欧氏几何题目能快速作图,并依据题目类型的不同,分别用不同的向量方法对其进行自动推理,证明结果简短可读.经过大量实例测试,证明将向量用于几何自动推理是可行和高效的.与《超级画板》等中的证明器相比,文中算法在自动推理能力和证明过程可读性方面有较大提高.文中给出的基于向量的几何可读证明算法丰富了几何定理自动推理方法,并且具有应用于几何教学实践的价值.     

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

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

一种新的基于扩展规则的定理证明算法

基于扩展规则的定理证明方法是一种与归结方法互补的新的定理证明方法,首先通过对扩展规则的深入研究,给出了扩展规则的一个重要性质,设计并实现了该性质的判定算法.此外,从理论上分析及证明了该判定算法的时问和空间复杂性.基于此,提出了一种新的基于扩展规则的定理证明算法NER,将判定子句集可满足性问题转化为一系列文字集合的包含问题,而非计数问题.实验结果表明,算法NER的执行效率较原有扩展规则算法IER和基于归结的有向归结算法DR有明显提高,有些问题可以提高两个数量级.     

Fast Theorem-Proving and Wu s Method

In this paper,the possibility of fast algorithm is discussed for mechanical theorem proving,where the degeneracy condition are considered in designing of these algorithms.It is found that all of the methods depend seriously on some principles appearing in Wu‘s Method.In other worsd,some principles in Wu‘s Method are the instinctive properties in these new fast algorithms of theorem proving.     

应用本体和AllegroGraph实现几何定理证明

由于传统的定理机器证明方法是基于规则的,使得定理证明出现几何信息增长迅猛,推理和计算效率低以及过程可读性差等问题。针对以上情况,提出了基于本体和AllegroGraph的几何定理证明方法。该方法通过本体构建几何定理命题模型,然后采用Prolog规则描述语言对几何定理性质进行描述,同时通过分析本体模型和规则描述的对应关系,提出定理规则半自动生成方法。最后以AllegroGraph（ AG）图形数据库的推理机制为基础,完成几何定理证明。实验结果表明,将本体和AllegroGraph推理机应用于几何定理证明领域可以摆脱以往几何定理证明代数化问题,几何证明过程容易理解,同时合理地控制了信息的增长,支持定理可持续证明。     

Theorem Proving Guided Development of Formal Assertions in a Resource-Constrained Scheduler for High-Level Synthesis

This paper presents a formal specification and a proof of correctness for the widely-used Force-Directed List Scheduling (FDLS) algorithm for resource-constrained scheduling of data flow graphs in high-level synthesis systems. The proof effort is conducted using a higher-order logic theorem prover. During the proof effort many interesting properties of the FDLS algorithm are discovered. These properties are formally stated and proved in a higher-order logic theorem proving environment. These properties constitute a detailed set of formal assertions and invariants that should hold at various steps in the FDLS algorithm. They are then inserted as programming assertions in the implementation of the FDLS algorithm in a production-strength high-level synthesis system. When turned on, the programming assertions (1) certify whether a specific run of the FDLS algorithm produced correct schedules and, (2) in the event of failure, help discover and isolate programming errors in the FDLS implementation.We present a detailed example and several experiments to demonstrate the effectiveness of these assertions in discovering and isolating errors. Based on this experience, we discuss the role of the formal theorem proving exercise in developing a useful set of assertions for embedding in the scheduler code and argue that in the absence of such a formal proof checking effort, discovering such a useful set of assertions would have been an arduous if not impossible task.     

有穷时间投影时序逻辑的完备公理系统

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF给出了NFG的构造算法,并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL的定理证明方法可方便用于并发系统的建模与验证.     

改进的几何定理机器证明的概率性算法

将几何定理机器证明的研究方法概括为确定性算法与概率性算法两大类,针对已有的确定性算法和概率性算法的证明速率偏低或占用内存过大等问题,提出一种改进的概率性算法。主要是在改进对多项式中独立变元次数的上界估计的算法的基础上,结合Schwartz-Zippel定理和统计学理论,通过随机检验若干实例来证明几何定理,并能控制证明结果不真的概率在给定的小范围内。通过改进的概率性算法,成功在2秒内证明出代数法难以证明的五圆定理。最后的多组对比实验进一步表明,改进的概率性算法具有明显高效性。     

多项式等式型几何定理的可读证明

目前的智能几何软件都使用基于搜索法的定理证明器作为推理引擎,其主要缺点是不能可读地证明涉及到几何量代数运算的几何定理,这极大地限制了智能几何软件的实际应用.对一类结论为几何量多项式等式的几何定理,文中提出了一种能给出可读证明的启发式搜索算法.该算法通过引入多项式的变形操作算子——标准项代换,把证明结论为多项式等式g=0的几何定理转化为寻找从g到0的标准项代换序列的搜索问题.采用Lisp语言实现了该算法,并做了30个结论为几何量等式的几何定理的推理实验.实验结果表明算法具有较高的推理效率.     

基于语义tableau的一阶逻辑自动定理证明

自动推理作为自动定理证明的扩展是人工智能研究的基础工作,许多重要的人工智能系统都是以推理系统为其核心部分,其中的tableau方法,由于具有通用性、直观性及易于计算机实现等特点,至今成为重要的自动推理方法之一。在tableau方法基础上,讨论了一阶逻辑中的自动定理证明理论,提出使用模型存在定理证明其可靠性和完备性的方法。同时也给出了带等词tableau方法的证明过程。