Sciweavers

Share
CADE
2006
Springer

Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems

10 years 8 months ago
Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems
Abstract. Semantic labelling is a transformational technique for proving termination of Term Rewriting Systems (TRSs). Only its variant with finite sets of labels was used so far in tools for automatic termination proving and variants with infinite sets of labels were considered not to be suitable for automation. We show that such automation can be achieved for semantic labelling with natural numbers, in combination with recursive path ordering (RPO). In order to do so we developed algorithms to deal with recursive path ordering for these infinite labelled systems. Using these techniques TPA, a tool developed by the first author, is the only current tool that can prove termination of the SUBST system automatically.
Adam Koprowski, Hans Zantema
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where CADE
Authors Adam Koprowski, Hans Zantema
Comments (0)
books