paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Tree-depth, quantifier elimination, and quantifier rank

树深度、量词消去与量词秩
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 1/10 · 该论文属于有限模型论与逻辑复杂度理论，研究树深度、量词消去与参数化模型检测，与用户关注的静态分析、LLM/Agent、浮点程序分析及贝叶斯程序分析没有直接关联。引用 6 inbox
Yijia Chen, Jörg Flum
逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：研究图类上有界树深度、FO 有效广义量词消去与参数化模型检测复杂度之间的等价关系。

论文研究有限图类 K 上三个性质之间的关系：K 的树深度是否有界；一阶逻辑 FO 在 K 上是否具有有效的广义量词消去；以及 FO 在 K 上的参数化模型检测是否属于 para-AC0。作者证明由有界树深度可推出有效广义量词消去，而有效广义量词消去与参数化模型检测属于 para-AC0 等价。进一步地，若 K 对取子图封闭，则三者完全等价；但一般情况下，树深度有界并不被后两者蕴含，因此三者不等价。该结果用树深度与量词消去刻画 FO 模型检测的参数化复杂度上界。

问题
刻画有限图类上一阶逻辑模型检测的参数化复杂度与量词消去、树深度有界性之间的关系。
方法
通过有限模型论与逻辑方法，证明三条性质之间的蕴含与等价，并区分图类是否对取子图封闭。
评估
以定理形式证明有界树深度推出有效广义量词消去，后者与 FO 参数化模型检测属于 para-AC0 等价；子图封闭时三者等价，一般情形不等价。
原文摘要（Abstract）

For a class K of finite graphs we consider the following three statements. (i) K has bounded tree-depth. (ii) First-order logic FO has an effective generalized quantifier elimination on K. (iii) The parameterized model checking for FO on K is in para-AC0. We prove that (i) ⟹ (ii) and (ii) ⟺ (iii). All three statements are equivalent if K is closed under taking subgraphs, but not in general.

链接与引用

DOI 原文 ·

BibTeX 
@inproceedings{paperbot4392,
  title = {Tree-depth, quantifier elimination, and quantifier rank},
  author = {Yijia Chen and Jörg Flum},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209160}
}