一句话：证明带中性字母的 Σ₂ 正则语言可由仅用序关系谓词的 Σ₂ 公式定义，推进 Straubing 中心猜想。
论文刻画带中性字母、可由一次交替一阶逻辑（Σ₂）定义的正则语言。作者证明：若任意 Σ₂ 公式定义了一个带中性字母的正则语言，则存在仅使用序关系谓词的等价 Σ₂ 公式。这验证了 Straubing 中心猜想在带中性字母语言上对 Σ₂ 的情形成立，也是该猜想二十多年来的首次进展。为获得该刻画，论文建立了针对顶扇入恒定的多项式大小深度-3 布尔电路的下界，其组合论证核心是研究语言中位置之间如何相互确定，该技术本身也具有独立价值。
The regular languages with a neutral letter expressible in first-order logic with one alternation are characterized. Specifically, it is shown that if an arbitrary Σ2 formula defines a regular language with a neutral letter, then there is an equivalent Σ2 formula that only uses the order predicate. This shows that the so-called Central Conjecture of Straubing holds for Σ2 over languages with a neutral letter, the first progress on the Conjecture in more than 20 years. To show the characterization, lower bounds against polynomial-size depth-3 Boolean circuits with constant top fan-in are developed. The heart of the combinatorial argument resides in studying how positions within a language are determined from one another, a technique of independent interest.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{BarloyCPZ22,
title = {The Regular Languages of First-Order Logic with One Alternation},
author = {Corentin Barloy and Michael Cadilhac and Charles Paperman and Thomas Zeume},
booktitle = {LICS},
year = {2022},
doi = {10.1145/3531130.3533371}
}