Nagele, Julian and Felgenhauer, Bertram and Zankl, Harald - Certifying Confluence Proofs via Relative Termination and Rule Labeling

lmcs:3654 - Logical Methods in Computer Science, May 11, 2017, Volume 13, Issue 2 - https://doi.org/10.23638/LMCS-13(2:4)2017
Certifying Confluence Proofs via Relative Termination and Rule Labeling

Authors: Nagele, Julian and Felgenhauer, Bertram and Zankl, Harald

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. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems.


Volume: Volume 13, Issue 2
Published on: May 11, 2017
Submitted on: May 11, 2017
Keywords: Computer Science - Logic in Computer Science,F.2,F.4


Share

Consultation statistics

This page has been seen 536 times.
This article's PDF has been downloaded 184 times.