Abstract

Relative termination, a generalized notion of termination, has been used in a number of different contexts like proving the confluence of rewrite systems or analyzing the termination of narrowing. In this paper, we introduce a new 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. The practical significance of our method is illustrated by means of an experimental evaluation.

BibTeX

@inproceedings{JINNGVAY-CADE15,
  author    = "Jos{\'e} Iborra and Naoki Nishida and Germán Vidal and
               Akihisa Yamada",
  title     = "Reducing Relative Termination to Dependency Pair Problems",
  booktitle = "Proceedings of the 25th International Conference on
               Automated Deduction (CADE-25)",
  editor    = "Amy Felty and Aart Middeldorp",
  series    = "Lecture Notes in Artificial Intelligence",
  volume    = 9195,
  pages     = "163--178",
  year      = 2015,
  doi       = "10.1007/978-3-319-21401-6_11"
}