HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Deduction versus Computation: the Case of Induction

Eric Deplagne 1 Claude Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The fundamental difference and the essential complementarity between computation and deduction are central in computer algebra, automated deduction, proof assistants and in frameworks making them cooperating. In this work we show that the fondamental proof method of induction can be understood and implemented as either computation or deduction. 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 work, 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.
Document type :
Conference papers
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 2:53:35 PM
Last modification on : Friday, February 4, 2022 - 3:33:25 AM


  • HAL Id : inria-00101024, version 1



Eric Deplagne, Claude Kirchner. Deduction versus Computation: the Case of Induction. Sixth International Conference on Artificial Intelligence and Symbolic Computation - AISC'2002, Jul 2002, Marseille, France, pp.4-6. ⟨inria-00101024⟩



Record views