On Proving Uniform Termination and Restricted Termination of Rewriting Systems
From MaRDI portal
Publication:3040518
DOI10.1137/0212012zbMath0526.68036OpenAlexW2090626768MaRDI QIDQ3040518
Deepak Kapur, J. V. Guttag, David R. Musser
Publication date: 1983
Published in: SIAM Journal on Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1137/0212012
confluenceterm rewriting systemscanonicalKnuth-Bendix algorithmequational axiomsrewrite rulesglobal finitenessoverlap closurerestricted terminationrewrite dominoesuniform termination
Related Items (18)
Meta-rule synthesis from crossed rewrite systems ⋮ On recursive path ordering ⋮ From Outermost Reduction Semantics to Abstract Machine ⋮ On relationship between term rewriting systems and regular tree languages ⋮ Termination of rewriting ⋮ The Church-Rosser property for ground term-rewriting systems is decidable ⋮ On deciding the confluence of a finite string-rewriting system on a given congruence class ⋮ It is decidable whether a monadic thue system is canonical over a regular set ⋮ Deciding Innermost Loops ⋮ Chain properties of rule closures ⋮ Overlap closures do not suffice for termination of general term rewriting systems ⋮ Loop detection in term rewriting using the eliminating unfoldings ⋮ Unnamed Item ⋮ Chain properties of rule closures ⋮ Loops under Strategies ⋮ Non-Looping String Rewriting ⋮ An \(O(| T| ^ 3)\) algorithm for testing the Church-Rosser property of Thue systems ⋮ A finite Thue system with decidable word problem and without equivalent finite canonical system
This page was built for publication: On Proving Uniform Termination and Restricted Termination of Rewriting Systems