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

Peiya Liu, Ruey-Juin Chang

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.