2026-07-20T05:44:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4072 2024-03-06T10:34:47Z ddc:004 open_access

Confluence by Decreasing Diagrams – Formalized Zankl, Harald term rewriting confluence decreasing diagrams formalization 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Harald Zankl 2013 Is Part Of LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2013.352 urn:nbn:de:0030-drops-40723 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.352 eng https://creativecommons.org/licenses/by/3.0/legalcode