Relative Termination via Dependency Pairs

José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada

Journal of Automated Reasoning 58(3), pp. 391 – 411, 2017.


A term rewrite system is terminating when no infinite reduction sequences are possible. Relative termination generalizes termination by permitting infinite reductions as long as some distinguished rules are not applied infinitely many times. Relative termination is thus a fundamental notion that has been used in a number of different contexts, like analyzing the confluence of rewrite systems or the termination of narrowing. In this work, we introduce a novel technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. We first present a general approach that is then instantiated to provide a concrete technique
for proving relative termination. The practical significance of our method is illustrated by means of an experimental evaluation.


  PDF |    doi:10.1007/s10817-016-9373-5  


author = "Jos{\'e} Iborra and Naoki Nishida and Germ{\'a}n Vidal and Akihisa Yamada",
title = "Relative Termination via Dependency Pairs",
journal = "Journal of Automated Reasoning",
year = 2017,
volume = 58,
number = 3,
pages = "391-411",
doi = "10.1007/s10817-016-9373-5"
Nach oben scrollen