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: rewriting, termination, well-founded ordering, recursive path ordering..
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
A Theorem on $N$-Tuples Which is Equivalent to the Well-Ordering Theorem.H. Rubin & J. E. Rubin - 1967 - Notre Dame Journal of Formal Logic 8 (1-2):48-50.
Strong Termination for the Epsilon Substitution Method.Grigori Mints - 1996 - Journal of Symbolic Logic 61 (4):1193-1205.
A Construction for Recursive Linear Orderings.C. J. Ash - 1991 - Journal of Symbolic Logic 56 (2):673-683.
The Independence of the Prime Ideal Theorem From the Order-Extension Principle.U. Felgner & J. K. Truss - 1999 - Journal of Symbolic Logic 64 (1):199-215.
Off-Line Parsability and the Well-Foundedness of Subsumption.Shuly Wintner & Nissim Francez - 1999 - Journal of Logic, Language and Information 8 (1):1-16.
Up to Equimorphism, Hyperarithmetic Is Recursive.Antonio Montalbán - 2005 - Journal of Symbolic Logic 70 (2):360 - 378.
Extensions of Arithmetic for Proving Termination of Computations.Clement F. Kent & Bernard R. Hodgson - 1989 - Journal of Symbolic Logic 54 (3):779-794.
The Order Types of Termination Orderings on Monadic Terms, Strings and Monadic Terms, Strings and Multisets.Ursula Martin & Elizabeth Scott - 1997 - Journal of Symbolic Logic 62 (2):624-635.
Added to index2009-01-28
Total downloads3 ( #696,714 of 2,168,955 )
Recent downloads (6 months)1 ( #346,364 of 2,168,955 )
How can I increase my downloads?