The rule labeling heuristic aims to establish confluence of (left-)linearterm rewrite systems via decreasing diagrams. We present a formalization of aconfluence criterion based on the interplay of relative termination and therule labeling in the theorem prover Isabelle. Moreover, we report on theintegration of this result into the certifier CeTA, facilitating the checkingof confluence certificates based on decreasing diagrams. The power of themethod is illustrated by an experimental evaluation on a (standard) collectionof confluence problems.
展开▼
