Modular Semantic Labeling and Unlabeling


Termination of term rewrite systems is an interesting and popular research
area. In the last years several methods have been developed to
automatically prove termination of term rewrite systems. Two popular
methods are the dependency pair framework and semantic labeling where
termination proofs are done by iteratively modifying the rewrite systems by
sound techniques until termination is trivially achieved.

For such an iterative method it is often useful to remove those labels that
have been introduced by the semantic labeling technique. The reason is that
otherwise, the rewrite systems easily become too large to process them
further. Here, it is essential that the decreasing rules are removed before
unlabeling is performed.  We show that unlabeling without decreasing rules
is unsound in general and show our solution to this problem. Moreover, we
also investigate semantic labeling and unlabeling in the setting of
dependency pairs where additional problems arise when dealing with minimal
chains.

Our work has been formally verified in the library IsaFoR (Isabelle
Formalization of Rewriting) and is used to certify termination proofs of
sizes up to several megabytes.