Predicting Failures of and Repairing Inductive Proof Attempts

Inductive reasoning is critical for ensuring reliability of computational descriptions, especially of algorithms defined on recursive data structures. Despite advances made in automating inductive reasoning, proof attempts by theorem provers frequently fail while performing inductive reasoning. A user of such a system must scrutinize a failed proof attempt and do intensive debugging to understand the cause of failure, and then provide additional information to make a failed proof attempt succeed. A method for predicting a priori failure of proof attempts by induction is proposed. It is based on analyzing the definitions of function symbols appearing in a conjecture. Further, failure analysis is shown to provide information that can be used to make those proof attempts succeed for valid conjectures. The failure of proof attempts could be because of a number of reasons even when a conjecture is believed to be valid. It might be that an induction scheme used in a proof attempt is not powerful enough to yield useful induction hypotheses which can be applied effectively. Or, even when induction hypotheses are applicable, the proof attempt might not succeed because of missing lemmas. A method for speculating intermediate lemmas which can make induction hypotheses applicable and/or lead to simplification obtaining validity is proposed. The analysis can be automated and is illustrated on several examples. A preliminary implementation demonstrates the effectiveness of the proposed approach.