Induction for weak termination

Isabelle Gnaedig 1 Olivier Fissore 1 Hélène Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We propose an original approach to prove weak termination of innermost rewriting on ground term algebras, based on induction, abstraction and narrowing. The abstraction mechanism schematizes the application of the induction hypothesis on terms, and narrowing schematizes reductions. The induction relation, an F-stable ordering having the subterm property, is not given a priori, but its existence is checked along the proof, by testing satisfiability of ordering constraints. An extension of the method is given, where the information given by abstraction are memorized and used. Our method is more specific than methods proving strong termination of rewriting under strategies, which also give a weak termination proof for the standard rewriting. Indeed, ours can in addition handle TRSs that are not strongly innermost terminating.
Type de document :
[Intern report] A02-R-111 || gnaedig02a, 2002, 23 p
Liste complète des métadonnées
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:55:09
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57


  • HAL Id : inria-00101056, version 1



Isabelle Gnaedig, Olivier Fissore, Hélène Kirchner. Induction for weak termination. [Intern report] A02-R-111 || gnaedig02a, 2002, 23 p. 〈inria-00101056〉



Consultations de la notice