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.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Adam Koprowski, Hans Zantema
• Keywords: Automated Reasoning, CADE 2006, Recursive Path, Semantic Labelling, Term Rewriting Systems