Coq 中 PCP 相关计算归约的验证
计算机科学中的逻辑
2022-12-09 v2 形式语言与自动机理论
摘要
我们使用证明辅助工具 Coq 正式验证了关于邮资对应问题（PCP）的若干计算归约。我们的验证包括将一个推广图灵机停机问题的字符串重写问题归约到 PCP，以及将 PCP 归约到上下文无关文法的交问题和回文问题。有趣的是，文献中某些归约的严格正确性证明是缺失的。
引用
@article{arxiv.1711.07023,
title = {Verification of PCP-Related Computational Reductions in Coq},
author = {Yannick Forster and Edith Heiter and Gert Smolka},
journal= {arXiv preprint arXiv:1711.07023},
year = {2022}
}