Extensions to the Rewrite Rule Laboratory and Research in Automated Deduction Based on Rewriting Techniques and Completion

一个名为RRL的软件系统，即重写规则实验室，在过去四年中开发，得到了以前NSF拨款的部分支持，既是一个定理证明者，也是一个试验和开发基于重写方法的新的自动推理程序的环境。RRL包括一组规则完成和重写算法的实现，这些算法可以用于证明谓词演算和结构归纳定理。RRL已被成功地用于解决通常被认为是机械化定理证明者的挑战的问题，包括在硬件和软件的验证和规范方面的重要应用。展望了RRL的进一步发展和关联理论的研究。重点将是开发和扩展RRL，使其更有用和更方便地推理软件和硬件规范和实现。为了实现这一目标，RRL将得到增强，以提供通过归纳法自动证明性质的强大方法。理论研究将结合两种不同的方法来自动进行归纳证明，一致性证明方法和显式归纳方法是在上一次NSF拨款下开发的。还将进一步研究分析规范结构性质的方法，如一致性和定义完备性性质，以及关于不完全规范的推理方法。将进行开发启发式算法的理论和实验研究，包括识别不必要的计算，以改进完成过程和一阶定理证明方法的性能。还将继续进行复杂性研究和基本运算的有效实施，并将把结果纳入RRL。

A software system called RRL, the Rewrite Rule Laboratory, developed over the past four years with partial support from previous NSF grants, is both a theorem prover and an environment for experimenting with and developing new automated reasoning procedures based on rewrite methods. RRL includes implementations of a collection of rule-completion and rewriting algorithms that can be applied to proving predicate calculus and structural induction theorems. RRL has been successfully used for solving problems often considered a challenge for mechanized theorem provers, including significant applications in verification and specification of hardware and software. Further development of RRL and research in the associated theory are proposed. The focus will be to develop and extend RRL to be more useful and convenient for reasoning about software and hardware specifications and implementations. Towards this goal, RRL will be enhanced to provide powerful methods for automatically proving properties by induction. Theoretical research will be undertaken to combine two different approaches for automating proofs by induction, the proof by consistency approach and the explicit induction approach developed under the last NSF grant. Further investigations will also be conducted on methods for analyzing structural properties of specifications such as the consistency and definitional completeness properties and for reasoning about incomplete specifications. Theoretical and experimental research in developing heuristics, including identifying unnecessary computations, will be undertaken to improve the performance of completion procedures and of first-order theorem proving methods. Complexity studies and efficient implementations of primitive operations will also be continued and results will be incorporated into RRL.