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.     

On the Complexity of Deduction Modulo Leaf Permutative Equations

In the context of equational reasoning, J. Avenhaus and D. Plaisted proposed to deal with leaf permutative equations in a uniform, specialized way. The simplicity of these equations and the useless variations that they produce are good incentives to lift theorem proving to so-called stratified terms, in order to perform deduction modulo such equations. This requires specialized algorithms for standard problems involved in automated deduction. To analyze the computational complexity of these problems, we focus on the group theoretic properties of stratified terms. NP-completeness results are given and (slightly) relieved by restrictions on leaf permutative theories, which allow the use of techniques from computational group theory.     

Using Satisfiability Modulo Theories for Inductive Verification of Lustre Programs

The problem of verifying safety properties of Lustre programs with integer arithmetic have been attacked in several different ways. Abstract interpretation is used in NBAC, and inductive verification using a SAT solver is used in Luke.This paper presents a method of using Satisfiability Modulo Theories (SMT) as an incremental decision procedure for inductive verification of Lustre program. We show that even a very naive approach using SMT is competitive and in some instances complementary to other approaches.     

Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005)

The Satisfiability Modulo Theories Competition (SMT-COMP) is intended to spark further advances in the decision procedures field, especially for applications in hardware and software verification. Public competitions are a well-known means of stimulating advancement in automated reasoning. Evaluation of SMT solvers entered in SMT-COMP took place while CAV 2005 was meeting. Twelve solvers were entered; 1,352 benchmarks were collected in seven different divisions.     

Simplifying Proofs in Fitch-Style Natural Deduction Systems

We present an algorithm for simplifying Fitch-style natural-deduction proofs in classical first-order logic. We formalize Fitch-style natural deduction as a denotational proof language,, with a rigorous syntax and semantics. Based on that formalization, we define an array of simplifying transformations and show them to be terminating and to respect the formal semantics of the language. We also show that the transformations never increase the size or complexity of a deduction – in the worst case, they produce deductions of the same size and complexity as the original. We present several examples of proofs containing various types of superfluous “detours,” and explain how our procedure eliminates them, resulting in smaller and cleaner deductions. All of the transformations are fully implemented in SML-NJ, and the complete code listing is available on the Web.     

命题逻辑中形式推演证明题的自动评阅系统

自动阅卷评分是大规模计算机考试的必然选择,而数学类主观题涉及运算符号、运算步骤、解题方法多样等问题,其自动评分一直制约着考试系统的发展。数理逻辑是数学的一个分支,命题逻辑是数理逻辑的一部分。命题逻辑的同一个形式可推演性模式可以有不同的形式证明,即存在一题多解的情况,但其证明有严格的程式,针对其特点用C#开发一个适用于其自身的自动评分系统。应用表明,系统操作界面友好,可大大提高教师阅卷的工作效率。     

求解极小SMT不可满足子式的宽度优先搜索算法

极小不可满足子式能够为可满足性模理论(SMT)公式的不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误.针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其3类结点的概念,并给出了不可满足子式、极小不可满足子式与3类结点之间的映射关系.基于这种映射关系,采用宽度优先的搜索策略提出了宽度优先搜索的极小SMT不可满足子式求解算法.基于业界公认的SMT Competition 2007测试集进行实验的结果表明,该算法能够有效地求解极小不可满足子式.     

相干命题逻辑系统R的一种演绎生成算法

本文提出了相干命题逻辑系统R的一种演绎生成算法--试探法。该算法采用后向推理法,依据推理规则将待证命题逐步分解成子命题并构造一棵证明树,对系统R中的定理证明取得了较好的效果。     

SMT求解技术的发展及最新应用研究综述

可满足性模理论(satisfiability modulo theories, SMT)是判定一阶逻辑公式在组合背景理论下的可满足性问题.SMT的背景理论使其能很好地描述实际领域中的各种问题,结合高效的可满足性判定算法,SMT在测试用例自动生成、程序缺陷检测、RTL(register transfer level)验证、程序分析与验证、线性逻辑约束公式优化问题求解等一些最新研究领域中有着突出的优势.首先阐述SMT问题的基础SAT(satisfiability)问题及判定算法;其次对SMT问题、判定算法进行了总结,分析了主流的SMT求解器,包括Z3,Yices2,CVC4等;然后着重介绍了SMT求解技术在典型领域中的实际应用,对目前的研究热点进行了阐述;最后对SMT未来的发展前景进行了展望,目的是试图推动SMT的发展,为此领域的相关人员提供有益的参考.     

命题逻辑提升到一阶逻辑上的子句消去方法

在基于命题逻辑的可满足性问题（SAT）求解器和基于一阶逻辑的定理证明器上，子句集简化一直是必不可少的步骤，而其中子句消去方法在这些子句集简化方法中是非常重要的组成部分。将命题逻辑中的子句消去方法归结隐藏恒真消去方法（RHTE）和归结隐藏包含消去方法（RHSE）提升到一阶逻辑上，并且利用蕴含模归结原则（IMR）证明了这种提升方式在一阶逻辑上具有可靠性（Soundness），即依据这两种子句消去方法删除一阶逻辑公式集中的子句，并不会改变公式集的可满足性或者不可满足性。此外，将这两个方法与一阶逻辑子句消去方法锁子句消去方法（BCE）和归结包含消去方法（RSE）进行组合推广，发展得到一阶逻辑上新型子句消去方法（BC+RHS）E、（RS+RHT）E和（RHS+RHT）E，并且证明了这3种子句消去方法在一阶逻辑上的可靠性。最后，分析比较了这些子句消去方法的有效性，并且证明了这3种新型子句消去方法比组成它们的原始子句消去方法均具有更高的有效性。     

避免模调度中cache代价的优化方法

软件流水能够加快循环的执行速度.模调度是一种被广泛采用的软件流水的启发式.为了改善存储系统,cache使用了分级机制,但这也带来了额外的存储延迟-cache代价.证明了模调度可能导致cache代价,并提出了一种可以避免模调度的cache代价的PCPMS(prevent cache penalty in modulo scheduling)算法.实验结果表明,PCPMS能够避免模调度中的cache代价,提高程序性能.     

Clausal resolution in a logic of rational agency

A resolution based proof system for a Temporal Logic of Possible Belief is presented. This logic is the combination of the branching-time temporal logic CTL (representing change over time) with the modal logic KD45 (representing belief ). Such combinations of temporal or dynamic logics and modal logics are useful for specifying complex properties of multi-agent systems. Proof methods are important for developing verification techniques for these complex multi-modal logics. Soundness, completeness and termination of the proof method are shown and simple examples illustrating its use are given.     

模调度与DFA结合的技术及其在gcc上的实现

循环是程序中的热代码,而软件流水是一种细粒度的循环优化方法,它通过将循环中不同迭代之间的操作并行执行,最大程度地开发指令级并行。模调度是一种效果很好的软件流水算法。论文以gcc3.3为基础,提出了模调度与DFA结合的软件流水方法,及其工程实现,实验数据表明,优化效果明显。     

SMS软件流水调度算法的设计与实现

循环是程序中的热代码,对循环进行有效的优化可以显著缩短程序的执行时间。软件流水是一种开发循环体指令级并行的细粒度循环优化技术,它通过调度循环中连续迭代之间的指令使其并行执行,从而提高了循环的执行效率。实验数据表明,用Cerngoop程序包进行测试,循环优化效果明显。     

真实环境下对幂剩余指数的SDPA攻击

介绍边信道攻击的概念和研究背景,研究幂剩余算法及BR算法从右至左的实现过程,指出在实际应用中,使用简单能量分析对幂剩余算法进行攻击时,攻击者需要了解算法的具体运算过程,同时还需具备一定经验,否则不易找到能量消耗曲线与指数信息之间的准确对应关系,且用户稍加防范即可使攻击失效。提出一种简单差分能量分析攻击方法,可以更容易地得到指数信息,并使实验结果更准确。通过真实环境下的实验,进一步证实了该方法的可行性和正确性。     

模2n加的异或差分概率的快速计算方法

分析模2n加变换的异或差分概率计算算法的计算复杂性,利用以空间换时间的思想,将该算法中的矩阵乘积运算预先计算并予以存储,从而以查表运算替代多个矩阵乘积运算等方法对模2n加变换的异或差分概率计算算法进行改进,改进后算法的计算复杂性小于现有方法计算复杂性的7.7%。     

归结原理及其应用

归结演绎推理是一种在计算机上得到较好实现的基于归结原理的推理技术,介绍归结原理的基本思想以及它在自动推理中的应用。