cl-banner

Proving Termination of Rewrite Systems using Bounds

Martin Korp and Aart Middeldorp

Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA 2007), Lecture Notes in Computer Science 4533, pp. 273 – 287, 2007.

Abstract

The use of automata techniques to prove the termination of string rewrite systems and left-linear term rewrite systems is advocated by Geser et al. in a recent sequence of papers. We extend their work to non-left-linear rewrite systems. The key to this extension is the introduction of so-called raise rules and the use of tree automata that are not quite deterministic. Furthermore, we present negative solutions to two open problems related to string rewrite systems.

 

  PDF |    doi:10.1007/978-3-540-73449-9_21  |  © Springer

BibTeX 

@inproceedings{KM-RTA07,
author = "Martin Korp and Aart Middeldorp",
title = "Proving Termination of Rewrite Systems using Bounds",
booktitle = "Proceedings of the 18th International Conference on
Rewriting Techniques and Applications",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
year = 2007,
volume = 4533,
pages = "273--287"
}
Nach oben scrollen