# "Term Partition" for Mathematical Induction

1 COPRIN - Constraints solving, optimization and robust interval analysis
CRISAM - Inria Sophia Antipolis - Méditerranée , ENPC - École des Ponts ParisTech
Abstract : A key new concept, {\em 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 {\em language of normal forms of the ground instances of $t$}. If $\A {\em monomorphic} set of axioms (rules) and$(a,b)$is a term partition of$t$, then the normal form (obtained by using$\Aany ground instance of $t$ can be divided'' into the normal forms (obtained by using $\Athe corresponding ground instances of$a$and$b$. Given a conjecture$t = s$to be checked for inductive validity in a theory$\Aartition $(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 of $\A The method is conceptually different to the classical theorem proving approaches since it tries to directly mechanize the$\omega\$-rule. It allows to obtain elegant and natural proofs of a large number of conjectures (including non-linear ones) without additional lemmas and/or generalizations.
Keywords :
Document type :
Reports
Domain :

Cited literature [1 references]

https://hal.inria.fr/inria-00072023
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 7:35:03 PM
Last modification on : Saturday, April 7, 2018 - 1:18:26 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:49:24 PM

### Identifiers

• HAL Id : inria-00072023, version 1

### Citation

Pascal Urso, Emmanuel Kounalis. "Term Partition" for Mathematical Induction. [Research Report] RR-4565, INRIA. 2002. ⟨inria-00072023⟩

Record views