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

重写规则实验室的扩展及基于重写技术和补全的自动推演研究

• 批准号: 8906678
• 负责人: Deepak Kapur
• 金额: $ 31.03万
• 依托单位: SUNY at Albany
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1989
• 资助国家: 美国
• 起止时间: 1989-09-15 至 1993-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8906678&HistoricalAwards=false
• 关键词: Extensions; Rewrite; Rule; Laboratory; Research

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.

一个名为RRL的软件系统，重写规则实验室， 在过去的四年里，部分支持从以前的国家科学基金会赠款， 既是一个定理证明器，也是一个实验环境， 开发基于重写方法的新的自动推理程序。 RRL包括规则完成集合的实现， 可用于证明谓词演算的重写算法 和结构归纳定理 RRL已成功用于 解决问题往往被认为是机械化定理的挑战 验证器，包括在核查方面的重要应用， 硬件和软件规格。 RRL的进一步发展和相关理论的研究是 提出了重点将是开发和扩展RRL，使其更有用 便于对软件和硬件规格进行推理 和实现。 为了实现这一目标，RRL将得到加强， 提供自动证明属性的强大方法， 诱导 理论研究将联合收割机和 不同的方法自动化证明归纳，证明由 一致性方法和显式归纳法的发展 在最后一次国家科学基金会资助下 进一步的调查也将 进行的方法，分析结构特性的 规范，如一致性和定义的完整性 属性和推理不完整的规范。 发展化学的理论和实验研究， 包括确定不必要的计算，将采取措施， 改进完成程序和一阶程序的执行情况 定理证明方法 复杂性研究和高效 原语操作的实现也将继续， 结果将纳入RRL。