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 fundamental 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Theorem proving modulo. Rapport de Recherche 3400, Institut National de Recherche en Informatique et en Automatique, April 1998. ftp://ftp.inria.fr/INRIA/publication/RR/RR-3400.ps.gz.
Gilles Dowek, Thérèse Hardin, and Claude Kirchner. HOL-λσ an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science, 11(1):21–45, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Deplagne, E., Kirchner, C. (2002). Deduction versus Computation: The Case of Induction. In: Calmet, J., Benhamou, B., Caprotti, O., Henocque, L., Sorge, V. (eds) Artificial Intelligence, Automated Reasoning, and Symbolic Computation. AISC Calculemus 2002 2002. Lecture Notes in Computer Science(), vol 2385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45470-5_3
Download citation
DOI: https://doi.org/10.1007/3-540-45470-5_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43865-6
Online ISBN: 978-3-540-45470-0
eBook Packages: Springer Book Archive