A New Structural Induction Scheme for Proving Properties of Mutually Recursive Concepts

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 6

Automated Reasoning

Structural induction schemes have been used for mechanically proving properties of self-recursive concepts in previous research. However, based on those schemes, it becomes very difficult to automatically generate the right induction hypotheses whenever the conjectures are involved with mutually recursive concepts. This paper will show that the difficulties come mainly from the weak induction schemes provided in the past, and a strong induction scheme is needed for the mutually defined concepts. Furthermore, a generalized induction principle is provided to smoothly integrate both schemes. Thus, in this mechanical induction, hypotheses are generated by mixing strong induction schemes with weak inductions schemes. While the weak induction schemes are suggested by self- recursive concepts, the strong induction schemes are suggested by mutually recursive concepts.