Induction for Termination - Archive ouverte HAL Access content directly
Reports Year : 1999

Induction for Termination

(1) , (1) ,
1

Abstract

We propose a new approach to prove termination of innermost rewriting, based on induction, abstraction and narrowing. The induction ordering is not explicitly given a priori, but its existence is checked along the proof, by testing satisfiability of ordering constraints. A rule-based description of the technique is given, as well as a few examples to illustrate the method.
Not file

Dates and versions

inria-00098943 , version 1 (26-09-2006)

Identifiers

  • HAL Id : inria-00098943 , version 1

Cite

Isabelle Gnaedig, Hélène Kirchner, Thomas Genet. Induction for Termination. [Intern report] 99-R-338 || gnaedig99a, 1999, pp.21. ⟨inria-00098943⟩
162 View
0 Download

Share

Gmail Facebook Twitter LinkedIn More