Abstract

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.

BibTeX

@article{INVY-JAR2017,
 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"
}