Bertram Felgenhauer

Deciding Confluence and Normal Form Properties of Ground Term Rewrite Systems Efficiently

2018 · DOAJ (DOAJ: Directory of Open Access Journals)

It is known that the first-order theory of rewriting is decidable for ground term rewrite systems, but the general technique uses tree automata and often takes exponential time. For many properties, including confluence (CR), uniqueness …