Recommendations
Cites work
- scientific article; zbMATH DE number 1729952 (Why is no real title available?)
- scientific article; zbMATH DE number 1322309 (Why is no real title available?)
- scientific article; zbMATH DE number 1543072 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- A reduction-preserving completion for proving confluence of non-terminating term rewriting systems
- Automated confluence proof by decreasing diagrams based on rule-labelling
- Combinatory logic. Vol. II
- Confluence by Decreasing Diagrams
- Confluence by decreasing diagrams
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Decreasing diagrams and relative termination
- Developing developments
- Generalizing Newman’s Lemma for Left-Linear Rewrite Systems
- Higher-order rewrite systems and their confluence
- Isabelle/HOL. A proof assistant for higher-order logic
- KBO orientability
- Labelings for Decreasing Diagrams.
- Matrix interpretations for proving termination of term rewriting
- Modular complexity analysis via relative complexity
- Modular properties of composable term rewriting systems
- On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
- Proving Confluence of Term Rewriting Systems Automatically
- Satisfiability of non-linear (ir)rational arithmetic
- Solving Partial Order Constraints for LPO Termination
- Tree-Manipulating Systems and Church-Rosser Theorems
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
- Decreasing diagrams with two labels are complete for confluence of countable systems
- Labelings for Decreasing Diagrams.
- Decreasing diagrams and relative termination
- Relative termination via dependency pairs
- Regular patterns in second-order unification
- 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
- Compositional confluence criteria
- Automated confluence proof by decreasing diagrams based on rule-labelling
- scientific article; zbMATH DE number 2043523 (Why is no real title available?)
- 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
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)
