paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On the Succinctness of Atoms of Dependency

论依赖原子的简洁性
LMCS vol.Volume 15, Issue 32019匹配度 1/10 · 该论文研究命题团队逻辑中依赖原子的简洁性,属于纯逻辑与自动机理论,与用户关注的静态分析、LLM/Agent、浮点程序分析及贝叶斯程序分析均无直接关联。引用 2 inbox
Martin Lück, Miikka Vilander
crossref: 2026-09-10

AI 速览

一句话:系统比较命题团队逻辑中各类依赖原子在存在片段与全片段下的简洁性,给出指数下界与多项式上界。

命题团队逻辑是命题层面的一阶团队逻辑,可表达 dependence、independence、inclusion、exclusion 和 anonymity 等非经典原子;但除 dependence 外,其余原子的翻译此前仅有指数规模构造。本文系统比较这些原子在存在片段(分离析取仅允许正出现)与带无限制否定的全命题团队逻辑中的简洁性。作者将 Ehrenfeucht–Fraïssé 博弈的变体 formula size game 引入团队逻辑,用于证明规模下界;在存在片段中对所有上述原子得到指数下界,而在全片段中对所有原子给出多项式上界。

问题
非经典依赖原子在命题团队逻辑中的表达简洁性差异不明,尤其除 dependence 外,其余原子此前仅已知指数规模的翻译。
方法
将 Ehrenfeucht–Fraïssé 博弈的变体 formula size game 引入团队逻辑,比较存在片段与全片段中各种原子翻译的公式规模。
评估
通过公式规模博弈证明存在片段中所有相关原子均需指数规模,并构造全片段中所有原子的多项式规模上界。
原文摘要(Abstract)

Propositional team logic is the propositional analog to first-order team logic. Non-classical atoms of dependence, independence, inclusion, exclusion and anonymity can be expressed in it, but for all atoms except dependence only exponential translations are known. In this paper, we systematically compare their succinctness in the existential fragment, where the splitting disjunction only occurs positively, and in full propositional team logic with unrestricted negation. By introducing a variant of the Ehrenfeucht-Fra\"{i}ss\'{e} game called formula size game into team logic, we obtain exponential lower bounds in the existential fragment for all atoms. In the full fragment, we present polynomial upper bounds also for all atoms.

链接与引用

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

BibTeX
@article{paperbot768,
  title = {On the Succinctness of Atoms of Dependency},
  author = {Martin Lück and Miikka Vilander},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 3},
  year = {2019},
  doi = {10.23638/lmcs-15(3:17)2019}
}