Certifying Confluence Proofs via Relative Termination and Rule Labeling

Julian Nagele, Bertram Felgenhauer, and Harald Zankl

Logical Methods in Computer Science, 13(2:4), pp. 1 – 27, 2017.


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.


  PDF |    doi:10.23638/LMCS-13(2:4)2017  


author = "Julian Nagele and Bertram Felgenhauer and Harald Zankl",
title = "Certifying Confluence Proofs via Relative Termination and Rule Labeling",
journal = "Logical Methods in Computer Science",
volume = 13,
number = "2:4",
pages = "1--27",
year = 2017,
doi = "10.23638/LMCS-13(2:4)2017"
Nach oben scrollen