半扩展规则下分解的定理证明方法

基于扩展规则的定理证明方法在一定意义上是与归结原理对偶的方法,通过子句集能否推导出所有极大项来判定可满足性.IER(improved extension rule)算法是不完备的算法,在判定子句集子空间不可满足时,并不能判定子句集的满足性,算法还需重新调用ER(extension rule)算法,降低了算法的求解效率.通过对子句集的极大项空间的研究,给出了子句集的极大项空间分解后子空间的求解方法.通过对扩展规则的研究,给出了极大项部分空间可满足性判定方法PSER(partial semi-extension rule).在IER算法判定子空间不可满足时,可以调用PSER算法判定子空间对应的补空间的可满足性,从而得到子句集的可满足性,避免了不能判定极大项子空间可满足性时需重新调用ER算法的缺点,使得IER算法更完备.在此基础上,还提出DPSER(degree partial semi-extension rule)定理证明方法.实验结果表明:所提出的DPSER和IPSER的执行效率较基于归结的有向归结算法DR、IER及NER算法有明显的提高.     

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

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

基于IMOM和IBOHM启发式策略的扩展规则算法

基于扩展规则的方法是一种定理证明方法.在IER(improved extension rule)扩展规则算法的基础上,提出了IMOM(improved maximum occurrences on clauses of maximum size)和IBOHM(improved BOHM)启发式策略,并将两种启发式策略用于IER算法中,有指导性地选择限定搜索空间的子句,设计并实现了算法IMOMH_IER和IBOHMH_IER.实验结果表明,由于这两种启发式策略能够选择较为合适的搜索空间,可以尽快地判定出原问     

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

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

基于扩展规则的模型计数与智能规划方法

提出命题扩展规则方法ER的一种高效实现.在此基础上,研究了扩展规则方法在3个领域的应用:提出一次性求解一系列相近SAT问题的快速算法nER;提出基于扩展规则的模型计数算法     

一个基于规范变换的定理证明方法

在规范变换方法的基础上,给出了在有序类规范上的归纳定理的证明方法。该方法避免了Ｊｏｕａｎｎａｕｄ－Ｋｏｕｎａｌｉｓ方法中所谓归纳可归约性检查这一很费时的过程,并且终止性检查不依赖于合流性检查。     

模态逻辑推理的翻译方法

文中研究了模态逻辑推理的翻译法，即把模态逻辑公式按照一定的规则翻译成经典逻辑公式，再用传统的定理器进行推理，文中指出，该方法在理论上保持了正规命题模态逻辑的可判定性，还给出了一些试验结果，说明该方法实际可行的。     

基于高阶逻辑的定理证明方法及其对策的应用

定理证明是形式化验证的主要方法之一,其中定理证明器的使用是难点。为了提高证明效率,论述HOL4系统中主要的三种证明方法:支持高级证明步骤。自动推理和化简器,为定理的证明提供了一个完整而通用的理论框架。详细说明了以上三种证明方法的相关对策的功能和应用环境,并为应用中可能出现的问题提出解决方案。给出的对策应用实例不仅体现了三种方法中相关对策的实用性,还进一步表明了提出解决方案的有效性。     

一阶谓词演算定理机器证明的余式方法

本文将一阶谓词泻算的证明转化为代数族的计算，从而获得了代数化的Ｈｅｒｂｒａｎｄ过程，双通过一阶多项式间的求余运算，给出了余式方法并评理服它的完备性。同时，我们证明了归结原理是余式方法的一种特例。     

命题逻辑可满足性问题的算法分析

1 引言可满足性问题(以下简称SAT)是问:对于一个命题逻辑公式,是否存在对其变元的一个真值赋值使之成立?这个问题在许多领域都有非常重要的意义,其快速求解算法的研究成为计算机科学的中心课题之一。例如在机器定理证明领域,某命题是否是一个和谐的公理集合的推论,这个问题归结为该命题的反面与该公理集合一起是否是不可满足的。通过量词消去技术和Herbrand定理的作用,谓词逻辑公式的不可满足性可以归结为命题逻辑公式的不可满足性。在知识库维护中,当知识以逻辑公式的形式表达时,知识库的一致性检查可以归结为命题逻辑公式的可满足性。在开放逻辑中,新事实是否与已有的知识矛盾,当遇到事实反驳时如何求得最大和谐的知识集,这些问题最后都要归结为命题逻辑公式的可满足性。1971年Cook首次证明了SAT是NP-完全的,从而大量的计算问题都可以归约到SAT。正是由于SAT的重要地位,各国学者对它进行了广泛而深入的研究。     

Theorem Proving Based on the Extension Rule

Methods based on resolution have been widely used for theorem proving since it was proposed. This paper presents a new method for theorem proving that uses the inverse of resolution and employs the inclusion-exclusion principle to circumvent the problem of space complexity. We prove its soundness and completeness. The concept of complementary factor is introduced to estimate its complexity. We also show that our method outperforms resolution-based methods in some cases. Thus it is potentially a complementary method to resolution-based methods. This revised version was published online in August 2006 with corrections to the Cover Date.     

基于Tableau的定理机器证明系统TableauTAP

使用SWI-PROLOG语言在微机上设计实现了基于tableau的定理证明系统TabIeauTAP。该系统可以证明不含等词的经典逻辑公式童耋譬逻辑公式，通过预处理自动生成tableau规则，因此容易对其功能进行扩展。应用该系统对TPTP的400个逻辑问题进行证明，实验结果表明，TableauTAP在时间和空间效率上都是比较高的。     

基于定理证明的内存安全性动态检测算法的正确性研究

随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具.这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测.但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程序的加入可能会改变源程序的行为及语义,二是插桩程序并不能有效保证内存安全.为了解决这些问题,文中提出...     

Theorem Proving Modulo

Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate computations and deductions in a clean way. The first contribution of this paper is to define a sequent calculus modulo that gives a proof-theoretic account of the combination of computations and deductions. The congruence on propositions is handled through rewrite rules and equational axioms. Rewrite rules apply to terms but also directly to atomic propositions. The second contribution is to give a complete proof search method, called extended narrowing and resolution (ENAR), for theorem proving modulo such congruences. The completeness of this method is proved with respect to provability in sequent calculus modulo. An important application is that higher-order logic can be presented as a theory in deduction modulo. Applying the ENAR method to this presentation of higher-order logic subsumes full higher-order resolution. This revised version was published online in August 2006 with corrections to the Cover Date.     

几何定理并行验证算法研究

几何定理证明的数值验证法以数值计算代替符号计算来提高效率,但是在实际应用中对复杂命题的解题效率还存在问题。该文尝试用并行计算方法来提高算法效率,分析了MPI编程模型下的任务划分、通信组织、任务调度等问题,并在MPICH2下实现了数值并行验证算法,对算法的并行性能指标进行了测试,得到了较好的结果。     

Verifying the SRT Division Algorithm Using Theorem Proving Techniques

We verify the correctness of an SRT division circuit similar to the one in the Intel Pentium processor. The circuit and its correctness conditions are formalized as a set of algebraic relations on the real numbers. The main obstacle to applying theorem proving techniques for hardware verification is the need for detailed user guidance of proofs. We overcome the need for detailed proof guidance in this example by using a powerful theorem prover called Analytica. Analytica uses symbolic algebra techniques to carry out the proofs in this paper with much less guidance than existing general purpose theorem provers require for algebraic reasoning.     

机械化定理证明研究综述

随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向.