Induction as Deduction Modulo

Eric Deplagne 1 Claude Kirchner 2
2 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Inductive proofs can be built either explicitly by making use of an induction principle or implicitly by using the so-called induction by rewriting and inductionless induction methods. When mechanizing proof construction, explicit induction is used in proof assistants and implicit induction is used in rewrite based automated theorem provers. The two approaches are clearly complementary but up to now there was no framework able to encompass and to understand uniformly the two methods. In this paper, we propose such an approach based on the general notion of deduction modulo. We extend slightly the original version of the deduction modulo framework and we provide modularity properties for it. We show how this applies to a uniform understanding of the so called induction by rewriting method and how this relates directly to the general use of an induction principle.
Type de document :
[Intern report] A04-R-468 || deplagne04a, 2004, 80 p
Liste complète des métadonnées
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:58:02
Dernière modification le : jeudi 11 janvier 2018 - 06:19:59
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 12:06:54



  • HAL Id : inria-00099871, version 1



Eric Deplagne, Claude Kirchner. Induction as Deduction Modulo. [Intern report] A04-R-468 || deplagne04a, 2004, 80 p. 〈inria-00099871〉



Consultations de la notice


Téléchargements de fichiers