| 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.
Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems
In
Proceedings of the 3rd International Joint Conference on Automated Reasoning
( IJCAR '06),
Seattle, WA, USA.
BibTeX:@inproceedings{slnat-IJCAR-06,
author = {Adam Koprowski and Hans Zantema},
title = {Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems},
booktitle = {Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR '06)},
year = {2006},
series = {Lecture Notes in Computer Science},
volume = {4130},
pages = {332--346},
} | 
