cl-banner

Confluence by Decreasing Diagrams – Formalized

Harald Zankl

Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 352 – 367, 2013.

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.

 

  PDF |    doi:10.4230/LIPIcs.RTA.2013352  |  © Creative Commons License – NC – ND

BibTeX 

@inproceedings{HZ-RTA13,
author = "Harald Zankl",
title = "Confluence by Decreasing Diagrams --- Formalized",
booktitle = "Proceedings of the 24th International Conference on Rewriting
Techniques and Applications",
editor = "Femke van Raamsdonk",
series = "Leibniz International Proceedings in Informatics",
volume = 21,
pages = "352--367",
year = 2013,
doi = "10.4230/LIPIcs.RTA.2013352"
}
Nach oben scrollen