Skip to Main content Skip to Navigation
Conference papers

Incorporating Decision Procedures in Implicit Induction

Alessandro Armando 1 Michaël Rusinowitch 2 Sorin Stratulat 1
1 DIST - Department of informatics, systems and telecommunications
2 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In 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."
Mots-clés : automated deduction decision procedure procédure de décision preuve automatique induction
Complete list of metadatas
https://hal.inria.fr/inria-00100610
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 2:48:08 PM
Last modification on : Wednesday, January 8, 2020 - 2:17:17 PM

Identifiers

  • HAL Id : inria-00100610, version 1

Collections

INRIA | CNRS | LORIA | UNIV-LORRAINE

Citation

Alessandro Armando, Michaël Rusinowitch, Sorin Stratulat. Incorporating Decision Procedures in Implicit Induction. 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning - CALCULEMUS'2001, 2001, Sienne, Italy, 16 p. ⟨inria-00100610⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

126

 

Contact                    Legal Notice                    Personal Data