cl-banner

Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems

Martin Korp and Aart Middeldorp

Proceedings of the 2nd International Conference on Language and Automata Theory and Application (LATA 2008), Lecture Notes in Computer Science 5196, pp. 321 – 332, 2008.

Abstract

The match-bound technique is a recent and elegant method to prove the termination of rewrite systems using automata techniques. To increase the applicability of the method we incorporate it into the dependency pair framework. The key to this is the introduction of two new enrichments which take the special properties of dependency pair problems into account.

 

  PDF |    doi:10.1007/978-3-540-88282-4_30  |  © Springer

BibTeX 

@inproceedings{MKAM-LATA08,
author = "Martin Korp and Aart Middeldorp",
title = "Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems",
booktitle = "Proceedings of the 2nd International Conference on
Language and Automata Theory and Applications",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
volume = 5196,
year = 2008,
pages = "321--332"
}
Nach oben scrollen