通过相对终止与规则标记认证合流证明
计算机科学中的逻辑
2020-05-13 v2
摘要
规则标记启发式旨在经由递减图建立（左）线性项重写系统的合流性。我们提出了在定理证明器 Isabelle 中基于相对终止与规则标记相互作用的合流准则的形式化。此外，我们报告了将此结果集成到认证器 CeTA 中，从而便于基于递减图的合流证书的检查。该方法的威力通过在（标准）合流问题集上的实验评估得到说明。
引用
@article{arxiv.1612.07195,
title = {Certifying Confluence Proofs via Relative Termination and Rule Labeling},
author = {Julian Nagele and Bertram Felgenhauer and Harald Zankl},
journal= {arXiv preprint arXiv:1612.07195},
year = {2020}
}