Incorporating Decision Procedures in Implicit Induction

Colloque sans acte à diffusion restreinte. internationale.International audienceIn the last decades the automation of reasoning by mathematical induction has been thoroughly investigated and several powerful techniques and heuristics have been put forward. However, when applied to proof obligations arising in practical applications, the level of automation achieved by existing induction provers is still unsatisfactory. As shown by Boyer and Moore, a higher level of automation can be achieved by the incorporation of decision procedures into induction provers. Yet in Boyer and Moore's approach the role of the decision procedure is confined to the simplification engine and this limits the possible usage of the decision procedure by the prover. In this paper we present an extension to Boyer and Moore's integration schema that enables the decision procedure to use suitably selected instances of the induction hypotheses. The induction proof method we consider is based on and combines Cover Set Induction and Constraint Contextual Rewriting and has been implemented in the SPIKE prover. Computer experiments on non-trivial verification problems give evidence of the effectiveness of our approach: the proof of the MJRTY algorithm does not need anymore user-defined tactics as it is the case with STeP and Nuprl. Moreover, we show that a reasoning specialist for non-linear arithmetic theory can be easily integrated.