Multi-Predicate Induction Schemes for Mutual Recursion

Abstract

Where mutually recursive data types are used in programming languages, etc., mutually recursive functions are usually required. Mutually recursive functions are also quite common for non-mutually recursive types. Reasoning about recursive functions requires some form of mathematical induction but there have been difficulties in adapting induction methods for simple recursion to the mutually recursive case. This paper proposes the use of multi-predicate induction schemes in the context of explicit induction and presents a proof method for their use within a proof planning system. An implementation in Clam has successfully planned proofs for a number of mutually recursive examples.