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.

翻译：本文提出了一种通用框架，为满足特定固定参数可处理性要求的一阶理论固定否定片段提供了保证多项式时间可判定性的充分条件。该框架使得我们能够在多项式时间内判定此类理论中具有任意存在量化、合取及固定数量否定符号的语句。Nguyen与Pak近期研究[SIAM J. Comput. 51(2): 1--31 (2022)]表明，Presburger算术（带加法与序关系的整数一阶理论）中一个限制更强的此类片段是NP难问题。与此形成对比的是，通过应用本框架，我们证明了弱Presburger算术（从Presburger算术中移除序关系而保留等式的理论）的固定否定片段具有多项式时间可判定性。我们进一步给出两个框架实例化的案例，分别证明了弱线性实数算术的固定否定片段，以及每个不等式至多包含一个变量的Presburger算术限制版本的固定否定片段，均具有多项式时间可判定性。