Failure analyses of inductive theorem provers
Mahadevan Subramaniam · 1996
The main goal of this thesis is to facilitate the use of induction based theorem provers. The approach taken is twofold: minimize user intervention in handling failure scenarios of these systems and reduce the overheads in customizing applications. A formal framework for predicting and fixing of failures of inductive proof attempts is developed. Sufficient conditions for predicting the failures of an inductive proof attempt are obtained based on the structure of the given conjecture and that of the available facts. New methods are proposed for generalizing conjectures and for generating induction strategies for automatically fixing failures. These methods overcome several limitations of the currently employed methods. Automating reasoning over different representations of a data structure involves considerable overheads since conversions among these representations have to be manually supplied. The use of semantic information about a data structure for automatically reconciling the use of different representations is proposed. The proposed approach is described using a decision procedure for Presburger arithmetic (the quantifier-free theory of numbers with the addition operation and relational predicates $>, <, ot=, =, \geq, \leq$) for performing semantic analysis. The utility of the approach in enhancing many theorem proving procedures including those employed for mechanizing induction and generalization is discussed.