HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

"Term Partition" for Mathematical Induction

Pascal Urso 1 Emmanuel Kounalis 1
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.
Document type :
Reports
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072023
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 7:35:03 PM
Last modification on : Friday, February 4, 2022 - 3:17:55 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:49:24 PM

Identifiers

  • HAL Id : inria-00072023, version 1

Collections

Citation

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

Share

Metrics

Record views

68

Files downloads

187