Abstract

This paper is concerned with methods that automatically prove termination of term rewrite systems. The aim of dummy elimination, a method to prove termination introduced by Ferreira and Zantema, is to transform a given rewrite system into a rewrite system whose termination is easier to prove. We show that dummy elimination is subsumed by the more recent dependency pair method of Arts and Giesl. More precisely, if dummy elimination succeeds in transforming a rewrite system into a so-called simply terminating rewrite system then termination of the given rewrite system can be directly proved by the dependency pair technique. Even stronger, using dummy elimination as a preprocessing step to the dependency pair technique does not have any advantages either. We show that to a large extent these results also hold for the argument filtering transformation of Kusakari et al.

BibTeX Entry

@inproceedings{GM-CADE00,
 author    = "J{\"u}rgen Giesl and Aart Middeldorp",
 title     = "Eliminating Dummy Elimination",
 booktitle = "Proceedings of the 17th International Conference on Automated
              Deduction",
 series    = "Lecture Notes in Artificial Intelligence",
 volume    = "1831",
 pages     = "309--323",
 year      = 2000,
 doi       = "10.1007/10721959\_25"
}