paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On the complexity of Maslov's class K̅

论 Maslov 类 K̅ 的复杂度
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 1/10 · 该论文研究一阶逻辑片段 Maslov 类 K 的可满足性复杂度，属于纯逻辑与自动机理论，与用户关注的静态分析、Agentic/LLM 程序分析、浮点程序分析、贝叶斯程序分析及 AI 与 PL 交叉均无直接关联。引用 2 inbox
Oskar Fiuk, Emanuel Kieronski, Vincent Michielini
逻辑与自动机
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话：证明 Maslov 类 K 具有指数模型性质，从而确定其可满足性问题是 NExpTime 完全的。

Maslov 类 K 是一阶逻辑中一个表达力较强的片段，其可满足性问题已知可判定，但精确复杂度长期未确定。本文证明 K 具有指数规模模型性质，即若公式可满足则存在指数大小模型，由此得到其可满足性问题是 NExpTime 完全的。方法上，作者使用为 K 定制的可满足性博弈，并新颖地将悖论性锦标赛图应用于复杂度分析。除主结果外，论文还给出文献中若干相关片段的新复杂度结果，并提出无等词的一致一维片段的一个新的可判定扩展。这些结果厘清了一阶逻辑可判定片段的复杂度版图，并展示了博弈与组合图论工具在其中的作用。

问题
确定 Maslov 类 K 这一具有可判定可满足性的一阶逻辑片段的精确复杂度，并研究相关片段的复杂度。
方法
使用为 K 定制的可满足性博弈，并新颖地应用悖论性锦标赛图进行复杂度分析。
评估
通过证明 K 的指数模型性质得到其可满足性问题的 NExpTime 完全性，并给出相关片段的新复杂度结果及一个新的可判定扩展。
原文摘要（Abstract）

Maslov's class K is an expressive fragment of First-Order Logic known to have decidable satisfiability problem, whose exact complexity, however, has not been established so far. We show that K has the exponential-sized model property, and hence its satisfiability problem is NExpTime-complete. Additionally, we get new complexity results on related fragments studied in the literature, and propose a new decidable extension of the uniform one-dimensional fragment (without equality). Our approach involves a use of satisfiability games tailored to K and a novel application of paradoxical tournament graphs.

链接与引用

DOI 原文 · DBLP

BibTeX 
@inproceedings{FiukKM24,
  title = {On the complexity of Maslov's class K̅},
  author = {Oskar Fiuk and Emanuel Kieronski and Vincent Michielini},
  booktitle = {LICS},
  year = {2024},
  doi = {10.1145/3661814.3662097}
}