@inbook{e566ba78975f44f692456b08c8451351,
title = "A general theorem on termination of rewriting",
abstract = "We re-express our theorem on the strong-normalisation of display calculi as a theorem about the well-foundedness of a certain ordering on first-order terms, thereby allowing us to prove the termination of systems of rewrite rules. We first show how to use our theorem to prove the well-foundedness of the lexicographic ordering, the multiset ordering and the recursive path ordering. Next, we give examples of systems of rewrite rules which cannot be handled by these methods but which can be handled by ours. Finally, we show that our method can also prove the termination of the Knuth-Bendix ordering and of dependency pairs.",
keywords = "Recursive path ordering, Rewriting, Termination, Well-founded ordering",
author = "Dawson, {Jeremy E.} and Rajeev Gor{\'e}",
year = "2004",
doi = "10.1007/978-3-540-30124-0_11",
language = "English",
isbn = "3540230246",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "100--114",
editor = "Jerzy Marcinkowski and Andrzej Tarlecki",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
address = "Germany",
}