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