Confluence by Decreasing Diagrams – Formalized

Author Harald Zankl



PDF
Thumbnail PDF

File

LIPIcs.RTA.2013.352.pdf
  • Filesize: 0.53 MB
  • 16 pages

Document Identifiers

Author Details

Harald Zankl

Cite AsGet BibTex

Harald Zankl. Confluence by Decreasing Diagrams – Formalized. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 352-367, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
https://doi.org/10.4230/LIPIcs.RTA.2013.352

Abstract

This paper presents a formalization of decreasing diagrams in the theorem prover Isabelle. It discusses mechanical proofs showing that any locally decreasing abstract rewrite system is confluent. The valley and the conversion version of decreasing diagrams are considered.
Keywords
  • term rewriting
  • confluence
  • decreasing diagrams
  • formalization

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