2013/07/30 by Amira Henaien, Sorin Stratulat · 4 citations
Computer Science · Mathematics · #Automated proof checking #Automated theorem proving #Axiom #Calculus (dental) #Computer science #Gas meter prover #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Machine learning #Mathematical induction #Mathematical proof #Mathematics #Programming language #Proof assistant #Schema (genetic algorithms) #Scripting language #Semantic Web and Ontologies #Theoretical computer science #cs.LO
paper · pdf · doi:10.4204/eptcs.122.9
published in Electronic Proceedings in Theoretical Computer Science 122, 97-108 (Open Publishing Association) · In Proceedings SCSS 2012, arXiv:1307.8029
openalex publication_date 2013/07/30 · arxiv created 2013/07/31 · arxiv updated 2013/08/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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.