Decreasing diagrams and relative termination
From MaRDI portal
Publication:438562
DOI10.1007/S10817-011-9238-XzbMATH Open1243.68199OpenAlexW1997678912MaRDI QIDQ438562FDOQ438562
Authors: Nao Hirokawa, Aart Middeldorp 
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
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 (19)
- Confluence by critical pair analysis revisited
- Composing proof terms
- A proof method for local sufficient completeness of term rewriting systems
- Reducing relative termination to dependency pair problems
- Labelings for Decreasing Diagrams.
- Decreasing diagrams with two labels are complete for confluence of countable systems
- Decreasing diagrams and relative termination
- Title not available (Why is that?)
- Regular patterns in second-order unification
- Relative termination via dependency pairs
- De Bruijn's weak diamond property revisited
- Certifying confluence proofs via relative termination and rule labeling
- Proving confluence of term rewriting systems via persistency and decreasing diagrams
- Automated confluence proof by decreasing diagrams based on rule-labelling
- Title not available (Why is that?)
- ProTeM: a proof term manipulator (system description)
- Labelings for decreasing diagrams
- Diagrammatic Confluence and Completion
- CoLL: a confluence tool for left-linear term rewrite systems
Uses Software
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)
