sign in
english version rss feed

inria-00072023, version 1

"Term Partition" for Mathematical Induction

Pascal Urso 1, Emmanuel Kounalis 1

N° RR-4565 (2002)

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.

  • Domain : Computer Science/Other
  • Keywords : MATHEMATICAL INDUCTION / AUTOMATED REASONING / EQUATIONAL REASONING / REWRITING
  • Internal note : RR-4565
 
  • inria-00072023, version 1
  • oai:hal.inria.fr:inria-00072023
  • From: 
  • Submitted on: Tuesday, 23 May 2006 19:35:03
  • Updated on: Wednesday, 18 November 2009 14:19:28
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...