From diagrammatic confluence to modularity

DOI10.1016/j.tcs.2012.08.030zbMath1253.68197OpenAlexW2001532324MaRDI QIDQ1929228

Jean-Pierre Jouannaud, Jiaxiang Liu

Publication date: 7 January 2013

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2012.08.030

zbMATH Keywords

confluencemodularitydecreasing diagramsrewriting modulocofinal derivationslocal cliffslocal peaks

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Layer Systems for Proving Confluence, Unnamed Item, Confluence: The Unifying, Expressive Power of Locality, Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modularity of confluence: A simplified proof
• Confluence by decreasing diagrams
• On the modularity of termination of term rewriting systems
• On theories with a combinatorial definition of 'equivalence'
• A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems
• Confluence by Decreasing Diagrams
• Modular Church-Rosser Modulo
• Modularity of Confluence
• Diagrammatic Confluence and Completion
• Completion of a Set of Rules Modulo a Set of Equations
• Complete Sets of Reductions for Some Equational Theories
• Proving refutational completeness of theorem-proving strategies
• Abstract canonical inference
• On the Church-Rosser property for the direct sum of term rewriting systems
• Tree-Manipulating Systems and Church-Rosser Theorems