A general theorem on termination of rewriting
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...[Show more]
|Collections||ANU Research Publications|
|Source:||Proceedings of the 18th Annual Conference of the European Association for Computer Science Logic (CSL 2004)|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.