inria-00072023, version 1
"Term Partition" for Mathematical Induction
Pascal Urso 1Emmanuel Kounalis 1
N° RR-4565 (2002)
Résumé : 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.
- 1 : COPRIN (INRIA Sophia Antipolis)
- INRIA – Ecole des Ponts ParisTech
- Domaine : Informatique/Autre
- Mots-clés : MATHEMATICAL INDUCTION / AUTOMATED REASONING / EQUATIONAL REASONING / REWRITING
- Référence interne : RR-4565
- inria-00072023, version 1
- http://hal.inria.fr/inria-00072023
- oai:hal.inria.fr:inria-00072023
- Contributeur : Rapport De Recherche Inria
- Soumis le : Mardi 23 Mai 2006, 19:35:03
- Dernière modification le : Mercredi 18 Novembre 2009, 14:19:28






Documents associés

Exporter