David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
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)
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library||
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
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 downloads3 ( #611,461 of 1,792,259 )
Recent downloads (6 months)1 ( #464,595 of 1,792,259 )
How can I increase my downloads?