Performing Implicit Induction Reasoning with Certifying Proof Environments

Amira Henaien
(LITA, Université de Lorraine, Ile du Saulcy, 57000, Metz, France and Higher School of Communication of Tunis (Sup'Com), University of Carthage, Tunisia)
Sorin Stratulat
(LITA, Université de Lorraine, Ile du Saulcy, 57000, Metz, France )

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.

In Adel Bouhoula, Tetsuo Ida and Fairouz Kamareddine: Proceedings Fourth International Symposium on Symbolic Computation in Software Science (SCSS 2012), Gammarth, Tunisia, 15-17 December 2012, Electronic Proceedings in Theoretical Computer Science 122, pp. 97–108.
Published: 30th July 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: