一句话：提出一个通用框架，给出固定否定符号数的一阶理论片段多项式时间可判定的充分条件，并应用于弱 Presburger 算术等理论。
本文研究一阶理论中仅允许固定数量否定符号的片段的可判定性与复杂度。作者提出一个通用框架，通过要求理论满足某种固定参数可处理性条件，为任意存在量化与合取、但否定符号数固定的句子给出多项式时间判定算法。该框架与已知结果形成对比：Nguyen 和 Pak 证明 Presburger 算术中更受限的此类片段已是 NP 难。作为应用，作者证明弱 Presburger 算术（以相等替代序关系）的固定否定片段可在多项式时间判定，并进一步给出弱线性实数算术以及每条不等式至多含一个变量的 Presburger 算术限制的多项式时间可判定性。
This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that adhere to certain fixed-parameter tractability requirements. It enables deciding sentences of such theories with arbitrary existential quantification, conjunction and a fixed number of negation symbols in polynomial time. It was recently shown by Nguyen and Pak [SIAM J. Comput. 51(2): 1--31 (2022)] that an even more restricted such fragment of Presburger arithmetic (the first-order theory of the integers with addition and order) is NP-hard. In contrast, by application of our framework, we show that the fixed negation fragment of weak Presburger arithmetic, which drops the order relation from Presburger arithmetic in favour of equality, is decidable in polynomial time. We give two further examples of instantiations of our framework, showing polynomial-time decidability of the fixed negation fragments of weak linear real arithmetic and of the restriction of Presburger arithmetic in which each inequality contains at most one variable.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2407-18420,
title = {On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories},
author = {Christoph Haase and Alessio Mansutti and Amaury Pouly},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 1},
year = {2026},
doi = {10.46298/lmcs-22(1:21)2026}
}