Lemma Generation and Failure Heuristics for an Induction Theorem Prover (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.