Authors
Claus-Peter Wirth
Title
History and Future of Implicit and Inductionless Induction: Beware the old jade and the zombie!
In
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
Springer
Up-to-dateness
Yes! (Oct. 21, 2002)
Abstract
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.
Review
Two complete Comments for authors on a short preliminary version
Full paper
Original
Version with minor updates
  • Format
    .ps.gz
    Size
    .09 Mbytes
  • Format
    .dvi
    Size
    .03 Mbytes