Decreasing diagrams and relative termination

DOI10.1007/s10817-011-9238-xzbMath1243.68199OpenAlexW1997678912MaRDI QIDQ438562

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

zbMATH Keywords

confluenceterm rewritingdecreasing diagramsrelative termination

Mathematics Subject Classification ID

Related Items (12)

A proof method for local sufficient completeness of term rewriting systems ⋮ Relative termination via dependency pairs ⋮ Unnamed Item ⋮ CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems ⋮ Reducing Relative Termination to Dependency Pair Problems ⋮ Regular Patterns in Second-Order Unification ⋮ Unnamed Item ⋮ Unnamed Item ⋮ De Bruijn's weak diamond property revisited ⋮ Confluence by critical pair analysis revisited ⋮ Composing proof terms ⋮ Labelings for decreasing diagrams

Uses Software

• Isabelle/HOL
• Tyrolean

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
• Higher-order rewrite systems and their confluence
• Confluence by decreasing diagrams
• Developing developments
• Isabelle/HOL. A proof assistant for higher-order logic
• Modular properties of composable term rewriting systems
• Combinatory logic. Vol. II
• Satisfiability of Non-linear (Ir)rational Arithmetic
• 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
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• 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.
• Modular Complexity Analysis via Relative Complexity
• Tree-Manipulating Systems and Church-Rosser Theorems
• Decreasing Diagrams and Relative Termination

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