Decreasing diagrams and relative termination

DOI10.1007/S10817-011-9238-XzbMATH Open1243.68199OpenAlexW1997678912MaRDI QIDQ438562FDOQ438562

Aart Middeldorp, Nao Hirokawa

Publication date: 31 July 2012

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

Full work available at URL: https://doi.org/10.1007/s10817-011-9238-x

Recommendations

• Decreasing diagrams and relative termination
• Labelings for Decreasing Diagrams.
• Labelings for decreasing diagrams
• Proving confluence of term rewriting systems via persistency and decreasing diagrams
• Automated confluence proof by decreasing diagrams based on rule-labelling

zbMATH Keywords

confluenceterm rewritingdecreasing diagramsrelative termination

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Satisfiability of Non-linear (Ir)rational Arithmetic
• Modular Complexity Analysis via Relative Complexity
• Title not available (Why is that?)
• Combinatory logic. Vol. II
• Title not available (Why is that?)
• Modular properties of composable term rewriting systems
• Matrix interpretations for proving termination of term rewriting
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Higher-order rewrite systems and their confluence
• Tree-Manipulating Systems and Church-Rosser Theorems
• Confluence by decreasing diagrams
• Developing developments
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems
• Labelings for Decreasing Diagrams.
• Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling.
• Decreasing Diagrams and Relative Termination
• On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
• KBO orientability

Cited In (15)

• Confluence by critical pair analysis revisited
• Composing proof terms
• Title not available (Why is that?)
• A proof method for local sufficient completeness of term rewriting systems
• CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems
• Labelings for Decreasing Diagrams.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Relative termination via dependency pairs
• De Bruijn's weak diamond property revisited
• Reducing Relative Termination to Dependency Pair Problems
• Title not available (Why is that?)
• Regular Patterns in Second-Order Unification
• Labelings for decreasing diagrams
• Diagrammatic Confluence and Completion

Uses Software

• Isabelle/HOL
• Tyrolean

This page was built for publication: Decreasing diagrams and relative termination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q438562)