Abstract

We introduce a new technique for proving termination of term rewriting systems. The technique, a specialization of Zantema's semantic labelling technique, is especially useful for establishing the correctness of transformation methods that attempt to prove termination by transforming term rewriting systems into systems whose termination is easier to prove. We apply the technique to modularity, distribution elimination, and currying, resulting in new results, shorter correctness proofs, and a positive solution to an open problem.

BibTeX Entry

@inproceedings{MOZ-CADE96,
 author    = "Aart Middeldorp and Hitoshi Ohsaki and Hans Zantema",
 title     = "Transforming Termination by Self-Labelling",
 booktitle = "Proceedings of the 13th International Conference on
              Automated Deduction",
 series    = "Lecture Notes in Artificial Intelligence",
 volume    = 1104,
 pages     = "373--386",
 year      = 1996,
 doi       = "10.1007/3-540-61511-3\_101"
}