Sciweavers

30
Voted
LOPSTR
2009
Springer

Goal-Directed and Relative Dependency Pairs for Proving the Termination of Narrowing

14 years 6 months ago
Goal-Directed and Relative Dependency Pairs for Proving the Termination of Narrowing
In this work, we first consider a goal-oriented extension of the dependency pair framework for proving termination w.r.t. a given set of initial terms. Then, we introduce a new result for proving relative termination in terms of a dependency pair problem. Both contributions put together allow us to define a simple and powerful approach to analyzing the termination of narrowing, an extension of rewriting that replaces matching with unification in order to deal with logic variables. Our approach could also be useful in other contexts where considering termination w.r.t. a given set of terms is also natural (e.g., proving the termination of functional programs).
José Iborra, Naoki Nishida, Germán V
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where LOPSTR
Authors José Iborra, Naoki Nishida, Germán Vidal
Comments (0)