Performing Implicit Induction Reasoning with Certifying Proof Environments

Abstract : Largely adopted by proof assistants, the conventional induction methods based on explicit induction schemas are non-reductive and local, at schema level. On the other hand, the implicit induction methods used by automated theorem provers allow for lazy and mutual induction reasoning. In this paper, we present a new tactic for the Coq proof assistant able to perform automatically implicit induction reasoning. By using an automatic black-box approach, conjectures intended to be manually proved by the certifying proof environment that integrates Coq are proved instead by the Spike implicit induction theorem prover. The resulting proofs are translated afterwards into certified Coq scripts.
Type de document :
Communication dans un congrès
SCSS'2012 - 4th International Symposium on Symbolic Computation in Software Science, Dec 2012, Gammarth, Tunisia. 2012
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00764909
Contributeur : Sorin Stratulat <>
Soumis le : jeudi 13 décembre 2012 - 16:01:20
Dernière modification le : jeudi 11 janvier 2018 - 06:25:24
Document(s) archivé(s) le : dimanche 18 décembre 2016 - 00:50:53

Fichier

document.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00764909, version 1

Collections

Citation

Amira Henaien, Sorin Stratulat. Performing Implicit Induction Reasoning with Certifying Proof Environments. SCSS'2012 - 4th International Symposium on Symbolic Computation in Software Science, Dec 2012, Gammarth, Tunisia. 2012. 〈hal-00764909〉

Partager

Métriques

Consultations de la notice

257

Téléchargements de fichiers

107