Automation of mathematical induction as part of the history of logic
Se ha publicado un artículo sobre la historia del razonamiento automático titulado Automation of mathematical induction as part of the history of logic.
Sus autores son
- J Strother Moore (de la University of Texas at Austin) y
- Claus-Peter Wirth (del King’s College London).
Su resumen es
We review the history of the automation of mathematical induction.
This article is further organized as follows.
§§ 4 and 5 offer a self-contained reference for the readers who are not familiar with the field of mathematical induction and its automation. In § 4 we introduce the essentials of mathematical induction. In § 5 we have to become more formal regarding recursive function definitions, their consistency, termination, and induction templates and schemes.
The main part is § 6, where we present the historically most important systems in automated induction, and discuss the details of software systems for explicit induction, with a focus on the 1970s. After describing the application context in § 6.1, we describe the following Boyer–Moore theorem provers: the Pure LISP Theorem Prover (§ 6.2) Thm (§ 6.3) Nqthm (§ 6.4), and ACL2 (§ 6.5). The most noteworthy remaining explicit- induction systems are sketched in § 6.6.
Alternative approaches to the automation of induction that do not follow the paradigm of explicit induction are discussed in § 7.
After summarizing the lessons learned in § 8, we conclude with § 9.