Confluence by critical pair analysis revisited

DOI10.1007/978-3-030-29436-6_19OpenAlexW2946412716MaRDI QIDQ2305423

Julian Nagele, Vincent van Oostrom, Nao Hirokawa, Michio Oyamaguchi

Publication date: 10 March 2020

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

zbMATH Keywords

confluenceterm rewritingdecreasing diagrams

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Unnamed Item ⋮ Unnamed Item

Uses Software

• Yices
• Saigawa
• Nagoya Termination Tool
• CoCoWeb

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Decreasing diagrams and relative termination
• Higher-order rewrite systems and their confluence
• Conditional rewriting logic as a unified model of concurrency
• Developing developments
• About the rewriting systems produced by the Knuth-Bendix completion algorithm
• Labelings for decreasing diagrams
• On theories with a combinatorial definition of 'equivalence'
• Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
• Layer Systems for Proving Confluence
• Confluence by Decreasing Diagrams
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A complete axiomatisation for the inclusion of series-parallel partial orders
• Term Rewriting and All That
• Decreasing diagrams with two labels are complete for confluence of countable systems
• Nagoya Termination Tool
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• 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: Confluence by critical pair analysis revisited