@inproceedings{c71f625f411447758299ce8965009d38,

title = "Termination of abstract reduction systems",

abstract = "We present a general theorem capturing conditions required for the termination of abstract reduction systems. We show that our theorem generalises another similar general theorem about termination of such systems. We apply our theorem to give interesting proofs of termination for typed combinatory logic. Thus, our method can handle most path-orderings in the literature as well as the reducibility method typically used for typed combinators. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. All proofs have been formally machine-checked in Isabelle/HOL.",

keywords = "Rewriting, Strong normalisation, Termination, Well-founded ordering",

author = "Dawson, {Jeremy E.} and Rajeev Gor{\'e}",

year = "2007",

language = "English",

isbn = "1920682465",

series = "Conferences in Research and Practice in Information Technology Series",

booktitle = "Theory of Computing 2007 - Proceedings of the Thirteenth Computing",

note = "Theory of Computing 2007 - 13th Computing: The Australasian Theory Symposium, CATS 2007 ; Conference date: 30-01-2007 Through 02-02-2007",

}