Proving Confluence of Term Rewriting Systems Automatically

DOI10.1007/978-3-642-02348-4_7zbMath1242.68125OpenAlexW1586794044MaRDI QIDQ3636821

Yoshihito Toyama, Jun-ichi Yoshida, Takahito Aoto

Publication date: 30 June 2009

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02348-4_7

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (15)

Unnamed Item ⋮ CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems ⋮ First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification ⋮ Decreasing diagrams and relative termination ⋮ Unnamed Item ⋮ Certifying proofs in the first-order theory of rewriting ⋮ Decreasing Diagrams and Relative Termination ⋮ CSI – A Confluence Tool ⋮ Ground confluence of order-sorted conditional specifications modulo axioms ⋮ Nominal Confluence Tool ⋮ Proving Confluence of Term Rewriting Systems Automatically ⋮ Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems ⋮ Conditions for confluence of innermost terminating term rewriting systems ⋮ Improving rewriting induction approach for proving ground confluence ⋮ Labelings for decreasing diagrams

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mechanizing and improving dependency pairs
• Confluence by decreasing diagrams
• Termination of term rewriting: Interpretation and type elimination
• Developing developments
• Modular properties of composable term rewriting systems
• Confluence by Decreasing Diagrams
• Proving Confluence of Term Rewriting Systems Automatically
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A new parallel closed condition for Church-Rosser of left-linear term rewriting systems
• Term Rewriting and All That
• Computer Science Logic
• On the Church-Rosser property for the direct sum of term rewriting systems
• Tree-Manipulating Systems and Church-Rosser Theorems
• Term Rewriting and Applications

This page was built for publication: Proving Confluence of Term Rewriting Systems Automatically