The Church-Rosser property for ground term-rewriting systems is decidable
From MaRDI portal
Publication:1100890
DOI10.1016/0304-3975(87)90100-9zbMath0641.68044OpenAlexW2036985061MaRDI QIDQ1100890
Publication date: 1987
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(87)90100-9
Church-Rosser propertyconfluencydecidabiltyground term-rewriting systemnondeterministic root-to-root automataroot-to-frontier automata
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (17)
Deciding confluence of certain term rewriting systems in polynomial time ⋮ Efficient ground completion ⋮ Decidability of confluence and termination of monadic term rewriting systems ⋮ Open problems in rewriting ⋮ More problems in rewriting ⋮ Problems in rewriting III ⋮ Equality and disequality constraints on direct subterms in tree automata ⋮ Intersection of finitely generated congruences over term algebra ⋮ Term rewriting restricted to ground terms. ⋮ On ground tree transformations and congruences induced by tree automata. ⋮ Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems ⋮ New Undecidability Results for Properties of Term Rewrite Systems ⋮ Reachability and confluence are undecidable for flat term rewriting systems ⋮ The $\Pi^0_2$ -Completeness of Most of the Properties of Rewriting Systems You Care About (and Productivity) ⋮ Restricted ground tree transducers ⋮ Derivation trees of ground term rewriting systems. ⋮ Undecidable Properties on Length-Two String Rewriting Systems
Cites Work
- On Proving Uniform Termination and Restricted Termination of Rewriting Systems
- Proving termination with multiset orderings
- Fast Decision Procedures Based on Congruence Closure
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Tree-Manipulating Systems and Church-Rosser Theorems
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: The Church-Rosser property for ground term-rewriting systems is decidable
