Integrating Implicit Induction Proofs into Certified Proof Environments

Sorin Stratulat 1, 2
2 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We give evidence of the direct integration and automated checking of implicit induction-based proofs inside certified reasoning environments, as that provided by the Coq proof assistant. This is the first step of a long term project focused on 1) mechanically certifying implicit induction proofs generated by automated provers like Spike, and 2) narrowing the gap between automated and interactive proof techniques inside proof assistants such that multiple induction steps can be executed completely automatically and mutual induction can be treated more conveniently. Contrary to the current approaches of reconstructing implicit induction proofs into scripts based on explicit induction tactics that integrate the usual proof assistants, our checking methodology is simpler and fits better for automation. The underlying implicit induction principles are separated and validated independently from the proof scripts that consist in a bunch of one-to-one translations of implicit induction proof steps. The translated steps can be checked independently, too, so the validation process fits well for parallelisation and for the management of large proof scripts. Moreover, our approach is more general; any kind of implicit induction proof can be considered because the limitations imposed by the proof reconstruction techniques no longer exist. An implementation that integrates automatic translators for generating fully checkable Coq scripts from Spike proofs is reported.
Type de document :
Communication dans un congrès
Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.320-335, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00525187
Contributeur : Ist Inria Nancy Grand Est <>
Soumis le : lundi 11 octobre 2010 - 13:23:16
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10

Identifiants

  • HAL Id : inria-00525187, version 1

Collections

Citation

Sorin Stratulat. Integrating Implicit Induction Proofs into Certified Proof Environments. Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.320-335, 2010, Lecture Notes in Computer Science. 〈inria-00525187〉

Partager

Métriques

Consultations de la notice

146