History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie!

Abstract. In this survey on implicit induction I recollect some memories on the history of implicit induction as it is relevant for future research on computer-assisted theorem proving, esp. memories that significantly differ from the presentation in a recent handbook article on “inductionless induction”. Moreover, the important references excluded there are provided here. In order to clear the fog a little, there is a short introduction to inductive theorem proving and a discussion of connotations of implicit induction like “descente infinie”, “inductionless induction”, “proof by consistency”, implicit induction orderings (term orderings), and refutational completeness. 1 What Is Inductive Theorem Proving (ITP)? Inductive reasoning can be seen as extending deductive reasoning in that infinite deductive proofs may be represented in a finite cyclic form, as suggested in the following example, where Γ(x0, y) is a proposition over the natural numbers, where ‘s’ d...

• Type: Conference
• Year: 2005
• Where: BIRTHDAY
• Authors: Claus-Peter Wirth
• Keywords: Applied Computing, BIRTHDAY 2005, Implicit Induction, Inductive Theorem Proving, Theorem Proving