Certifying Confluence Proofs via Relative Termination and Rule LabelingArticle
Authors: Julian Nagele ; Bertram Felgenhauer ; Harald Zankl
NULL##NULL##NULL
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.
From Confluence to Unique Normal Forms: Certification and Complexity; Funder: Austrian Science Fund (FWF); Code: P 27528
Bibliographic References
1 Document citing this article
Christina Kohl;Aart Middeldorp, Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems, 2023, Boston MA USA, 10.1145/3573105.3575667.