2026-07-20T05:41:29Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5202 2024-03-06T10:36:03Z ddc:004 open_access

Certified Rule Labeling Nagele, Julian Zankl, Harald term rewriting confluence decreasing diagrams certification The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the integration of this result into the certifier CeTA, facilitating the checking of confluence certificates based on decreasing diagrams for the first time. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Julian Nagele and Harald Zankl 2015 Is Part Of LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2015.269 urn:nbn:de:0030-drops-52024 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.269 eng https://creativecommons.org/licenses/by/3.0/legalcode