Abstract

We give the first mechanized proof of the fact that for showing termination
of a term rewrite system, we may restrict to well-formed terms using just
the function symbols actually occurring in the rules of the system. Or
equivalently, termination of a term rewrite system is preserved under
signature extensions. We did not directly formalize the existing proofs for
this well-known result, but developed a new and more elegant proof by
reusing facts about dependency pairs.

We also investigate signature extensions for termination proofs that use
dependency pairs. Here, we were able to develop counterexamples which
demonstrate that signature extensions are unsound in general. We further
give two conditions where signature extensions are still possible.

BibTeX

@inproceedings{NHAM-IJCAR10,
  author      = "Christian Sternagel and Ren{\'e} Thiemann",
  title       = "Signature Extensions Preserve Termination -- An
                 Alternative Proof via Dependency Pairs",
  booktitle   = "Proceedings of the 19th Annual Conference of the European
                 Association for Computer Science Logic",
  series      = "Lecture Notes in Computer Science",
  volume      = 6247,
  pages       = "514--528",
  publisher   = "Springer-Verlag",
  year        = 2010
}