Layer Systems for Proving Confluence

DOI10.1145/2710017zbMath1354.68138arXiv1404.1225OpenAlexW2176474378MaRDI QIDQ2946770

Bertram Felgenhauer, Harald Zankl, Vincent van Oostrom, Aart Middeldorp

Publication date: 17 September 2015

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1404.1225

zbMATH Keywords

persistenceconfluenceterm rewritingmodularity

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (4)

Unification of drags and confluence of drag rewriting ⋮ Unnamed Item ⋮ Confluence by critical pair analysis revisited ⋮ Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs

Uses Software

• CSI
• Decreasing Diagrams
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modularity of confluence: A simplified proof
• Confluence by decreasing diagrams
• Termination of term rewriting: Interpretation and type elimination
• Confluence of curried term-rewriting systems
• Modular properties of composable term rewriting systems
• Comparing curried and uncurried rewriting
• From diagrammatic confluence to modularity
• Confluence by Decreasing Diagrams – Formalized
• Modularity of Confluence
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Term Rewriting and All That
• CSI – A Confluence Tool
• Labelings for Decreasing Diagrams.
• On the Church-Rosser property for the direct sum of term rewriting systems
• Tree-Manipulating Systems and Church-Rosser Theorems

This page was built for publication: Layer Systems for Proving Confluence