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.