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

Induction for Termination

(1) , (1) ,


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)


  • HAL Id : inria-00098943 , version 1


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


Gmail Facebook Twitter LinkedIn More