cl-banner

Reducing Relative Termination to Dependency Pair Problems

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

Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Artificial Intelligence 9195, pp. 163 – 178, 2015.

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.

 

  PDF |    doi:10.1007/978-3-319-21401-6_11  |  ©  Springer International Publishing Switzerland

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"
}
Nach oben scrollen