Termination of Priority Rewriting - Extended version - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2008

Termination of Priority Rewriting - Extended version



Introducing priorities in rewriting increases the expressive power of rules and helps to limit computations. Priority rewriting is used in rule-based programming as well as in functional programming. Termination of priority rewriting is then important to guarantee that programs give a result. We describe an inductive proof method for termination of priority rewriting, relying on an explicit induction on the termination property and working by generating proof trees, which model the rewriting relation by using abstraction and narrowing.
Fichier principal
Vignette du fichier
version-hal-lata.pdf (266.71 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

inria-00349031 , version 1 (22-03-2009)
inria-00349031 , version 2 (31-03-2009)


  • HAL Id : inria-00349031 , version 2


Isabelle Gnaedig. Termination of Priority Rewriting - Extended version. [Research Report] 2008. ⟨inria-00349031v2⟩
104 View
96 Download


Gmail Facebook Twitter LinkedIn More