Decreasing Diagrams and Relative Termination

DOI10.1007/978-3-642-14203-1_41zbMath1291.68347OpenAlexW1609605580MaRDI QIDQ5747786

Aart Middeldorp, Nao Hirokawa

Publication date: 14 September 2010

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_41

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Decreasing diagrams and relative termination

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
• KBO orientability
• Matrix interpretations for proving termination of term rewriting
• Diagram techniques for confluence
• Confluence by decreasing diagrams
• Developing developments
• Modular properties of composable term rewriting systems
• Confluence by Decreasing Diagrams
• Solving Partial Order Constraints for LPO Termination
• Generalizing Newman’s Lemma for Left-Linear Rewrite Systems
• Proving Confluence of Term Rewriting Systems Automatically
• Diagrammatic Confluence and Completion
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A geometric proof of confluence by decreasing diagrams
• Theory and Applications of Satisfiability Testing
• Tree-Manipulating Systems and Church-Rosser Theorems
• Term Rewriting and Applications