paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Multi-Structural Games and Number of Quantifiers

多结构博弈与量词数量
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 1/10 · 该论文属于有限模型论与逻辑中的量词数刻画,与用户关注的程序静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析均无直接关联。引用 5 inbox
Ronald Fagin, Jonathan Lenchner, Kenneth W. Regan, Nikhil Vyas
crossref: 2026-09-12

AI 速览

一句话:提出多结构博弈,以 r 轮胜负刻画分离两组结构所需一阶量词数,并完整判定线性序区分所需量词数。

论文研究多结构博弈(multi-structural games),它在两组结构 A 与 B 上进行,是 Ehrenfeucht–Fraïssé 博弈的推广。经典 EF 博弈刻画一阶句子的量词秩,而多结构博弈刻画量词数量:Spoiler 在 r 轮博弈中获胜,当且仅当存在一个至多含 r 个量词的一阶句子 φ,使 A 中每个结构都满足 φ,而 B 中每个结构都不满足 φ。作者利用该博弈完整刻画了区分不同大小线性序所需的一阶量词数量,并发展了可分析线性序之外更一般结构的组合工具。该工作为量词数量这一资源度量提供了博弈论框架与精细结果。

问题
如何用博弈论方法刻画一阶句子的量词数量,而不仅是量词秩?
方法
定义在两组结构 A 与 B 上进行的多结构博弈,证明 r 轮 Spoiler 胜利等价于存在至多 r 个量词的 FO 句子区分 A 与 B。
评估
用该博弈完整刻画区分不同大小线性序所需量词数,并发展分析线性序之外结构的工具。
原文摘要(Abstract)

We study multi-structural games, played on two sets ${\mathcal{A}}$ and ${\mathcal{B}}$ of structures. These games generalize Ehrenfeucht-Fraïssé games. Whereas Ehrenfeucht-Fraïssé games capture the quantifier rank of a first-order sentence, multi-structural games capture the number of quantifiers, in the sense that Spoiler wins the r-round game if and only if there is a first-order sentence ϕ with at most r quantifiers, where every structure in ${\mathcal{A}}$ satisfies ϕ and no structure in ${\mathcal{B}}$ satisfies ϕ. We use these games to give a complete characterization of the number of quantifiers required to distinguish linear orders of different sizes, and develop machinery for analyzing structures beyond linear orders.

链接与引用

DOI 原文 ·

BibTeX
@inproceedings{paperbot6191,
  title = {Multi-Structural Games and Number of Quantifiers},
  author = {Ronald Fagin and Jonathan Lenchner and Kenneth W. Regan and Nikhil Vyas},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470756}
}