RANKING 的形式化分析
计算机科学中的逻辑
2023-03-01 v2 数据结构与算法
摘要
我们描述了 RANKING（一种用于在线二分匹配的在线算法）的形式化正确性证明。我们形式化的一个结果是，它表明该算法的所有组合证明中都存在一个漏洞。填补该漏洞构成了本工作投入的主要精力。尽管该算法是被研究最多的算法之一，也是理论计算机科学中的核心结果。这一漏洞是形式化图形论证（在计算理论中无处不在）所面临困难的一个例证。
关键词
引用
@article{arxiv.2302.13747,
title = {A Formal Analysis of RANKING},
author = {Mohammad Abdulaziz and Christoph Madlener},
journal= {arXiv preprint arXiv:2302.13747},
year = {2023}
}