Julian Nagele ; Bertram Felgenhauer ; Harald Zankl - 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 LabelingArticle

Authors: Julian Nagele ; Bertram Felgenhauer ; Harald Zankl

    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
    Accepted on: May 11, 2017
    Submitted on: May 11, 2017
    Keywords: Computer Science - Logic in Computer Science,F.2,F.4
    Funding:
      Source : OpenAIRE Graph
    • From Confluence to Unique Normal Forms: Certification and Complexity; Funder: Austrian Science Fund (FWF); Code: P 27528

    1 Document citing this article

    Consultation statistics

    This page has been seen 1431 times.
    This article's PDF has been downloaded 335 times.