Labelings for decreasing diagrams

DOI10.1007/S10817-014-9316-YMaRDI QIDQ2352504zbMATH OpenOpenAlexWikidataFDO

Authors Harald Zankl, Bertram Felgenhauer, Aart Middeldorp

Publication date 2 July 2015

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

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10817-014-9316-y

zbMATH Keywords

automationconfluencedecreasing diagramsterm rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

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

Cites work

• A new parallel closed condition for Church-Rosser of left-linear term rewriting systems
• A reduction-preserving completion for proving confluence of non-terminating term rewriting systems
• A rewriting view of simple typing
• Automated confluence proof by decreasing diagrams based on rule-labelling
• Confluence by decreasing diagrams
• Confluence by Decreasing Diagrams
• Confluence by decreasing diagrams -- formalized
• Confluence of non-left-linear TRSs via relative termination
• Confluence without termination via parallel critical pairs
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• CSI -- a confluence tool
• Decreasing diagrams and relative termination
• Developing developments
• scientific article; zbMATH DE number 1543072 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Labelings for Decreasing Diagrams.
• Layer systems for proving confluence
• On the Church-Rosser property for the direct sum of term rewriting systems
• Proving Confluence of Term Rewriting Systems Automatically
• Semantics of order-sorted specifications
• Term Rewriting and All That
• Tree-Manipulating Systems and Church-Rosser Theorems

Cited in

(15)

• Confluence by critical pair analysis revisited
• Confluence by Decreasing Diagrams
• Decreasing diagrams and relative termination
• Decreasing diagrams with two labels are complete for confluence of countable systems
• Decreasing diagrams for confluence and commutation
• Proving confluence of term rewriting systems via persistency and decreasing diagrams
• Certified rule labeling
• Labelings for Decreasing Diagrams.
• Automated confluence proof by decreasing diagrams based on rule-labelling
• Decreasing diagrams and relative termination
• Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
• Compositional confluence criteria
• Sort-based confluence criteria for non-left-linear higher-order rewriting
• Simulating dependency pairs by semantic labeling
• Confluence of logically constrained rewrite systems revisited

Describes a project that uses

Uses Software

• CSI
• Archive of Formal Proofs
• Decreasing Diagrams

This page was built for publication: Labelings for decreasing diagrams

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