Advertisement
Published in:
2008 | OriginalPaper | Chapter
Root-Labeling
Authors : Christian Sternagel, Aart Middeldorp
Published in: Rewriting Techniques and Applications
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
In 2006
Jambox
, a termination prover developed by Endrullis, surprised the termination community by winning the string rewriting division and almost beating
AProVE
in the term rewriting division of the international termination competition. The success of
Jambox
for strings is partly due to a very special case of semantic labeling. In this paper we integrate this technique, which we call root-labeling, into the dependency pair framework. The result is a simple processor with help of which
T
T
T
2
surprised the termination community in 2007 by producing the first automatically generated termination proof of a string rewrite system with non-primitive recursive complexity (Touzet, 1998). Unlike many other recent termination methods, the root-labeling processor is trivial to automate and completely unsuitable for producing human readable proofs.