Confluence by Decreasing Diagrams – Formalized

Zankl, Harald

doi:10.4230/LIPIcs.RTA.2013.352

Document

Confluence by Decreasing Diagrams – Formalized

Author Harald Zankl

Part of: Volume: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: International Conference on Rewriting Techniques and Applications (RTA)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2013-06-24

PDF

File

PDF

LIPIcs.RTA.2013.352.pdf

Filesize: 0.53 MB
16 pages

Document Identifiers

DOI: 10.4230/LIPIcs.RTA.2013.352
URN: urn:nbn:de:0030-drops-40723

Subject Classification

Keywords

term rewriting
confluence
decreasing diagrams
formalization

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get 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

Author Details

Harald Zankl

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail