“Term Partition” for Mathematical Induction

A key new concept, term partition, allows to design a new method for proving theorems whose proof usually requires mathematical induction. A term partition of a term t is a well-defined splitting of t into a pair (a, b) of terms that describes the language of normal forms of the ground instances of t.If $$ \mathcal{A} $$ is a monomorphic set of axioms (rules) and (a, b) is a term partition of t, then the normal form (obtained by using $$ \mathcal{A} $$) of any ground instance of t can be “divided” into the normal forms (obtained by using $$ \mathcal{A} $$) of the corresponding ground instances of a and b. Given a conjecture t = s to be checked for inductive validity in the theory of A, a partition (a, b) of t and a partition (c, d) of s is computed. If a = c and b = d, then t = s is an inductive theorem for $$ \mathcal{A} $$.The method is conceptually different to the classical theorem proving approaches. It allows to obtain proofs of a large number of conjectures (including non-linear ones) without additional lemmas or generalizations.