Certifying Confluence Proofs via Relative Termination and Rule Labeling

TL;DR

This paper introduces a formalized confluence criterion using relative termination and rule labeling, implemented in Isabelle and integrated into CeTA, with experimental validation on standard confluence problems.

Contribution

It formalizes a confluence proof method combining relative termination and rule labeling within Isabelle and integrates it into CeTA for certificate checking.

Findings

Successful formalization in Isabelle

Effective integration into CeTA for certificate verification

Positive experimental results on standard confluence problems

Abstract

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.