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
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.


Source : oai:arXiv.org:1612.07195
DOI : 10.23638/LMCS-13(2:4)2017
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

Browsing statistics

This page has been seen 58 times.
This article's PDF has been downloaded 28 times.