Induction using term orders

We present a procedure for proving inductive theorems which is based on explicit induction, yet supports mutual induction. Mutual induction allows the postulation of lemmas whose proofs use the theorems ex hypothesi while the theorems themselves use the lemmas. This feature has always been supported by induction procedures based on Knuth-Bendix completion, but these procedures are limited by the use of rewriting (or rewriting-like) inferences. Our procedure avoids this limitation by making explicit the implicit induction realized by these procedures. As a result, arbitrary deduction mechanisms can be used while still allowing mutual induction. A preliminary version of this paper appeared in the proceedings of the 12th Conference on Automated Deduction, A. Bundy, editor. This author was supported by a grant from the Ministère des Affaires Etrangères, France.