Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling

Author Takahito Aoto



PDF
Thumbnail PDF

File

LIPIcs.RTA.2010.7.pdf
  • Filesize: 149 kB
  • 10 pages

Document Identifiers

Author Details

Takahito Aoto

Cite AsGet BibTex

Takahito Aoto. Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 7-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
https://doi.org/10.4230/LIPIcs.RTA.2010.7

Abstract

Decreasing diagrams technique (van Oostrom, 1994) is a technique that can be widely applied to prove confluence of rewrite systems. To directly apply the decreasing diagrams technique to prove confluence of rewrite systems, rule-labelling heuristic has been proposed by van Oostrom (2008). We show how constraints for ensuring confluence of term rewriting systems constructed based on the rule-labelling heuristic are encoded as linear arithmetic constraints suitable for solving the satisfiability of them by external SMT solvers. We point out an additional constraint omitted in (van Oostrom, 2008) that is needed to guarantee the soundness of confluence proofs based on the rule-labelling heuristic extended to deal with non-right-linear rules. We also present several extensions of the rule-labelling heuristic by which the applicability of the technique is enlarged.
Keywords
  • Confluence
  • Decreasing Diagrams
  • Automation
  • Term Rewriting Systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail