Razborov's flag algebra forms a powerful framework for deriving asymptotic inequalities between induced subgraph densities, underpinning many advances in extremal graph theory. This survey introduces flag algebra to computer scientists working in logic, programming languages, automated verification, and formal methods. We take a logical perspective on flag algebra and present it in terms of syntax, semantics, and proof strategies, in a style closer to formal logic. One popular proof strategy derives valid inequalities by first proving inequalities in a labelled variant of flag algebra and then transferring them to the original unlabelled setting using the so-called downward operator. We explain this strategy in detail and highlight that its transfer mechanism relies on the notion of what we call an adjoint pair, reminiscent of Galois connections and categorical adjunctions, which appear frequently in work on automated verification and programming languages. Along the way, we work through representative examples, including Mantel's theorem and Goodman's bound on Ramsey multiplicity, to illustrate how mathematical arguments can be carried out symbolically in the flag algebra framework.

翻译：拉兹博罗夫旗代数为推导诱导子图密度间的渐近不等式提供了强大框架，支撑了极值图论领域的诸多进展。本综述面向逻辑、编程语言、自动验证及形式化方法领域的计算机科学家介绍旗代数。我们从逻辑视角切入，以更贴近形式逻辑的风格，通过语法、语义与证明策略三方面呈现该理论。一种常用证明策略通过先在旗代数的标记变体中证明不等式，再利用所谓向下算子将其迁移至原始无标记场景，从而推导有效不等式。我们详细阐释该策略，并指出其迁移机制依赖于我们称为伴随对的概念——这一概念令人联想到伽罗瓦连接与范畴论中的伴随函子，在自动验证与编程语言研究中频繁出现。文中通过包括曼特尔定理与古德曼关于拉姆齐多重性的界在内的典型算例，展示如何在该框架下符号化地执行数学论证。