Dependency pairs are one of the most powerful techniques for proving termination of term rewrite systems (TRSs), and they are used in almost all tools for termination analysis of TRSs. Problem #106 of the RTA List of Open Problems asks for an adaption of dependency pairs for relative termination. Here, infinite rewrite sequences are allowed, but one wants to prove that a certain subset of the rewrite rules cannot be used infinitely often. Dependency pairs were recently adapted to annotated dependency pairs (ADPs) to prove almost-sure termination of probabilistic TRSs. In this paper, we develop a novel adaption of ADPs for relative termination. We implemented our new ADP framework in our tool AProVE and evaluate it in comparison to state-of-the-art tools for relative termination of TRSs.

翻译：依赖对是证明项重写系统（TRSs）终止性最强大的技术之一，被几乎所有TRS终止性分析工具所采用。RTA开放问题列表中的第106号问题要求将依赖对方法适配到相对终止场景。在此场景中，虽然允许无限重写序列，但需要证明重写规则的特定子集不能被无限次使用。最近，依赖对被扩展为带注释的依赖对（ADPs）用于证明概率TRS的几乎必然终止性。本文提出了一种新颖的ADP适配方法以解决相对终止问题。我们在自主研发的AProVE工具中实现了这一新型ADP框架，并与当前最先进的相对终止TRS工具进行了对比评估。