Skip to Main content Skip to Navigation
New interface

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.
Document type :
Complete list of metadata
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 2:55:09 PM
Last modification on : Thursday, October 27, 2022 - 1:45:02 PM


  • 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⟩



Record views