s'authentifier
version française rss feed

inria-00072023, version 1

"Term Partition" for Mathematical Induction

Pascal Urso 1, Emmanuel 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.

  • Domaine : Informatique/Autre
  • Mots-clés : MATHEMATICAL INDUCTION / AUTOMATED REASONING / EQUATIONAL REASONING / REWRITING
  • Référence interne : RR-4565
 
  • inria-00072023, version 1
  • oai:hal.inria.fr:inria-00072023
  • Contributeur : 
  • Soumis le : Mardi 23 Mai 2006, 19:35:03
  • Dernière modification le : Mercredi 18 Novembre 2009, 14:19:28
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...