- 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
- 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.
- Full paper
- Original: PDF
- Version with minor updates: PS.GZ