paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Group Order Logic

群阶逻辑
LICS 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2025匹配度 1/10 · 论文属于有限模型论与描述复杂性,研究带群阶算子的不动点逻辑及其多项式时间模型检测,与用户关注的静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析均无直接关联。引用 0 inbox
Anatole Dahan
crossref: 2026-09-12

AI 速览

一句话:提出带群阶算子的不动点逻辑 FP+ord,可多项式时间模型检测,并刻画更广的多项式时间可计算查询。

本文针对不动点逻辑 FP 无法刻画多项式时间可计算查询 P 的问题,引入群阶算子 ord,用于计算由可定义置换集合生成的群的阶。该算子是秩算子 rk 的推广,由此得到新逻辑 FP + ord,并把它作为 P 的新候选逻辑。作者证明 FP + ord 的模型检测仍是多项式时间可计算的;进一步,Lichter 最近工作中用于区分 FP + rk 与 P 的查询可在 FP + ord 中定义。证明关键在于在 FP + ord 内表达图规范化群论方法的一个片段,并据此规范化具有交换颜色的结构,而该结构类包含 Lichter 的反例。

问题
研究如何通过扩展不动点逻辑来逼近或刻画多项式时间可计算查询 P,并处理 FP + rk 仍无法定义 Lichter 反例查询的局限。
方法
在 FP 中加入群阶算子 ord,用于计算可定义置换生成群的阶,并在该逻辑中表达图规范化群论方法的一个片段。
评估
从理论上证明 FP + ord 的模型检测为多项式时间,证明 Lichter 的分离查询可在 FP + ord 中定义,并证明该逻辑可规范化具有交换颜色的结构。
原文摘要(Abstract)

We introduce an extension of fixed-point logic (FP) with a group-order operator (ord), that computes the size of a group generated by a definable set of permutations. This operation is a generalization of the rank operator (rk). We show that FP + ord constitutes a new candidate logic for the class of polynomial-time computable queries (P). As was the case for FP + rk, the model-checking of FP + ord formulae is polynomial-time computable. Moreover, the query separating FP + rk from P exhibited by Lichter in his recent breakthrough is definable in FP + ord. Precisely, we show that FP + ord canonizes structures with Abelian colors, a class of structures which contains Lichter’s counter-example. This proof involves expressing a fragment of the group-theoretic approach to graph canonization in the logic FP + ord.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot8634,
  title = {Group Order Logic},
  author = {Anatole Dahan},
  booktitle = {LICS},
  year = {2025},
  doi = {10.1109/lics65433.2025.00025}
}