
doi: 10.1007/10721959_25
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.
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 4 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
