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
Type de document :
Communication dans un congrès
9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning - CALCULEMUS'2001, 2001, Sienne, Italy, 16 p, 2001
Liste complète des métadonnées
https://hal.inria.fr/inria-00100610
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:48:08
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00100610, version 1

Collections

INRIA | 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, 2001. 〈inria-00100610〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

107

Contact


archive-ouverte@inria.fr