Lemma Generation and Failure Heuristics for an Induction Theorem Prover (RRL)

该项目在一个称为重写规则实验室(RRL)的基于归纳和重写规则的定理证明器中扩展了归纳方案的引理生成、启发式和失败分析。寻找合适的归纳法和推测中间引理是归纳法证明机械化的关键步骤。要使定理证明器对应用程序有效，定理证明器必须能够自动执行在应用程序领域中被视为例行公事的推理步骤。这可以在相当大的程度上借助用于对应用领域建模的数据结构的决策过程来实现。此外，这些决策程序应该与其他推理步骤和启发式紧密结合，包括简化(重写)、归纳方案的生成及其相对于成功可能性的分析、引理推测以及证明尝试所需的定义和引理的适当实例化。受硬件验证应用的启发，本项目致力于设计和实现比特、比特向量、数字、列表和序列以及数组等数据结构的决策过程，并将它们集成到基于归纳的证明器RRL中。

This project extends the lemma generation heuristics and failure analysis of induction schemes in an induction and rewrite-rule based theorem prover called Rewrite Rule Laboratory (RRL). Finding an appropriate induction scheme and speculation of intermediate lemmas are critical steps in mechanization of proofs by induction. For theorem provers to be effective for applications, it is essential that a theorem prover be able to automatically perform inference steps considered routine in the application domain. This can be achieved, to a considerable extent, with the help of decision procedure for data structures used to model the application domain. Further, these decision procedures should be tightly integrated with other inference steps and heuristics including simplification (rewriting), generation of induction schemes and their analysis vis a vis likelihood of success, lemma speculation, and appropriate instantiations of definitions and lemmas needed in proof attempts. Motivated by the application of hardware verification, this project seeks to design and implement decision procedures for data structures including bits, bit vectors, numbers, lists and sequences, and arrays, and integrate them in the induction based prover RRL.