一句话：在 Isabelle 中形式化相对终止与规则标记结合的合流性判定准则，并集成到 CeTA 以检查基于递减图的合流证书。
该论文关注项重写系统合流性的机器可检查认证问题。规则标记启发式通过递减图来判定（左）线性项重写系统的合流性，但相关判定准则缺乏形式化保证。作者在 Isabelle 证明助手中形式化了一个基于相对终止与规则标记相互作用的合流性判定准则，并将该结果集成到证书检查器 CeTA 中，使其能够检查基于递减图的合流性证书。论文还在标准合流问题集合上进行了实验评估，展示了该方法的实际能力。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{NageleFZ16,
title = {Certifying Confluence Proofs via Relative Termination and Rule Labeling},
author = {Julian Nagele and Bertram Felgenhauer and Harald Zankl},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 2},
year = {2017},
doi = {10.23638/lmcs-13(2:4)2017}
}