Incorporating Decision Procedures in Implicit Induction

In this paper we present an approach to integrating reasoning specialists into cover set induction based on constraint contextual rewriting. The approach has been successfully used to incorporate decision procedures into the SPIKE prover. Computer experiments on non-trivial verification problems illustrating the effectiveness of the proposed technique are given. The generality of the approach allows for the integration of computer algebra algorithms and techniques into induction theorem provers. To illustrate this, we discuss the integration of the Buchberger algorithm into our framework.