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).

• Type: Conference
• Year: 2009
• Where: LOPSTR
• Authors: José Iborra, Naoki Nishida, Germán Vidal
• Keywords: Artificial Intelligence, Dependency Pair, Dependency Pair Framework, Dependency Pair Problem, LOPSTR 2009