RULE-BASED INDUCTION

Induction is indispensable for reasoning about parameterized logical models, as they arise in the context of hardware and software verification. Sophisticated heuristics for mechanizing induction proofs exist and have been successfully implemented in theorem provers for first-order logic. This article is a presentation of a complementary induction method that makes extensive use of the expressiveness of higher-order logic and higher-order unification facilities of LAMBDA. Rather than hard-coded routines, rules are used that incarnate induction schemes in a concise way. By means of instantiatable meta-variables, these rules are more general and preserve the flexibility to gradually specify an induction scheme throughout a proof process, as more and more information is available, rather than fully determining the induction scheme right at the beginning. Safe inference mechanisms and general-purpose proof automation utilities in the proof checker LAMBDA are well-suited for an interactive induction assistant that integrates automatic induction heuristics and at they same time accepts human guidance.