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.
CITATION STYLE
Bronsard, F., Reddy, U. S., & Hasker, R. W. (1994). Induction using term orderings. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 814 LNAI, pp. 102–117). Springer Verlag. https://doi.org/10.1007/3-540-58156-1_8
Mendeley helps you to discover research relevant for your work.