Mahadevan Subramaniam, Deepak Kapur, and Stephan Falke:
Predicting Failures of and Repairing Inductive Proof Attempts
In Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems (Proceedings of the GM R&D Workshop).
Pages 177-192, 2007. ©Springer-Verlag
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.
[
BibTeX
|
Preliminary Version (ps.gz)
|
Preliminary Version (pdf)
|
Paper on SpringerLink
]