A Dependency Pair Framework for Relative Termination of Term Rewriting
Authors: J.-C. Kassing, G. Vartanyan, J. Giesl
Dependency pairs (DPs) are one of the most powerful techniques for proving termination of term rewrite systems (TRSs). A combination of a main TRS and a base TRS is relatively terminating if there is no rewrite sequence that uses infinitely many steps with rules from the main TRS (whereas rules from the base TRS may be used infinitely often). While a direct application of standard DPs to relative termination is not possible (Problem #106 of the RTA List of Open Problems), we introduce a new notion of annotated dependency pairs (ADPs) suitable for relative termination and develop the first dependency pair framework specifically targeting relative termination. We implemented our new framework in the tool AProVE and evaluate it in comparison to state-of-the-art tools for relative termination of TRSs. This is an extended abstract of our IJCAR ‘24 paper.