"Automation of Mathematical Induction as part of the History of Logic."

J Strother Moore, Claus-Peter Wirth (2013)
a service of Schloss Dagstuhl - Leibniz Center for Informatics