Razborov旗代数作为极值图论证明系统的导论
编程语言
2026-01-21 v1 计算机科学中的逻辑
组合数学
摘要
Razborov的旗代数构成了推导诱导子图密度之间渐近不等式的强大框架，支撑了极值图论的许多进展。本综述向从事逻辑、编程语言、自动验证和形式化方法的计算机科学家介绍旗代数。我们从逻辑的角度审视旗代数，并以更接近形式逻辑的风格，从语法、语义和证明策略方面进行阐述。一种流行的证明策略是首先在旗代数的带标签变体中证明不等式，然后使用所谓的向下算子将其转移到原始的无标签设置中。我们详细解释了这一策略，并强调其转移机制依赖于我们称之为伴随对的概念，这让人联想到Galois连接和范畴伴随，它们经常出现在自动验证和编程语言的研究中。在此过程中，我们通过代表性示例（包括Mantel定理和Goodman关于Ramsey多重性的界）进行讲解，以说明数学论证如何在旗代数框架内以符号方式执行。
引用
@article{arxiv.2601.12741,
title = {An Introduction to Razborov's Flag Algebra as a Proof System for Extremal Graph Theory},
author = {Gyeongwon Jeong and Seonghun Park and Hongseok Yang},
journal= {arXiv preprint arXiv:2601.12741},
year = {2026}
}