A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems

DOI10.2168/LMCS-8(1:31)2012zbMath1238.68071MaRDI QIDQ2881099

Yoshihito Toyama, Takahito Aoto

Publication date: 3 April 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

completionconfluenceequational term rewriting systemsconfluence modulo equations

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (6)

CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems ⋮ Modularity in term rewriting revisited ⋮ From diagrammatic confluence to modularity ⋮ How to prove decidability of equational theories with second-order computation analyser SOL ⋮ Unnamed Item ⋮ Labelings for decreasing diagrams

This page was built for publication: A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems