Mathematical Induction
Christoph Walther · 1994
Abstract Proving statements of arithmetic usually requires induction. Statements like are well-known from basic mathematics courses and provide beginner’s exercises for applying the induction principle. If we prove such statements we often appeal to our ‘intuition’ and use our knowledge about arithmetic without being aware of each decision made during the search for a proof. Of course, this is not required as long as we are successful in proving theorems by induction. But if we intend to automate induction theorem proving our proof-strategic knowledge must be made explicit such that a computer can perform the right decisions when searching for a proof.