Claus-Peter Wirth
History and Future of Implicit and Inductionless Induction: Beware the old jade and the zombie!
Mechanizing Mathematical Reasoning: Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday.
LNAI 2605, pp. 192-203, Springer.
Bibtex Entry
Copyright Owner
I recollect some memories on the history of implicit induction as it is relevant for future research on computer-assisted theorem proving, especially memories that significantly differ from the presentation in a recent handbook article on ``inductionless induction''. Moreover, the important references excluded there are provided here. 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.
Full paper