Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories

Christoph Haase, Alessio Mansutti, Amaury Pouly

TL;DR

This paper develops a general, representation-based framework to achieve polynomial-time decidability for fixed-$k$ negation fragments of first-order theories, provided the underlying signature satisfies certain uniform, parameterised tractability conditions. Central to the approach is the difference normal form, which accommodates negation and quantification in a controlled way, together with parametrised reductions (UXP) and a structured handling of projections. The authors instantiate the framework for weak linear real arithmetic and weak Presburger arithmetic, proving PTIME decidability for fixed-$k$ negations and enabling extraction of solution representations, in contrast to NP-hard results for certain stronger fragments. The framework offers a flexible methodology to analyze other FO extensions and abstract domains, potentially guiding tractability analyses in broader logical and arithmetic settings.

Abstract

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.

On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories

TL;DR

This paper develops a general, representation-based framework to achieve polynomial-time decidability for fixed- negation fragments of first-order theories, provided the underlying signature satisfies certain uniform, parameterised tractability conditions. Central to the approach is the difference normal form, which accommodates negation and quantification in a controlled way, together with parametrised reductions (UXP) and a structured handling of projections. The authors instantiate the framework for weak linear real arithmetic and weak Presburger arithmetic, proving PTIME decidability for fixed- negations and enabling extraction of solution representations, in contrast to NP-hard results for certain stronger fragments. The framework offers a flexible methodology to analyze other FO extensions and abstract domains, potentially guiding tractability analyses in broader logical and arithmetic settings.

Abstract

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.
Paper Structure (31 sections, 38 theorems, 65 equations, 4 figures)

This paper contains 31 sections, 38 theorems, 65 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Structure of this paper.
  3. Related work.
  4. Preliminaries
  5. Sets and functions
  6. Structures with indexed families of functions
  7. First-order theories (finite tuples semantics)
  8. Fixed negations fragments
  9. Representations and parametrised complexity of signatures
  10. Representations
  11. Implementations and computability
  12. Parametrised complexity of signatures
  13. A framework for the fixed negation fragment of first-order theories
  14. Ideas underlying the framework
  15. What the framework achieves.
  16. ...and 16 more sections

Key Result

Proposition 1

Deciding two-variables $\exists\forall$ weak PA Horn sentences is NP-hard.

Figures (4)

  • Figure 1: Illustration of the relative universal projection $\pi_Z^\forall(y,X)$.
  • Figure 2: Computing Boolean operations on SDFs.
  • Figure 3: Implementation of $\oplus \in \{\lor,\land,-\}$ as a $(\mathop{\mathrm{dep}}\nolimits(\theta)^2,\mathop{\mathrm{dep}}\nolimits(\theta))$-UXP reduction.
  • Figure 4: Implementation of $\leq$ as a $(\mathop{\mathrm{dep}}\nolimits(\theta)^2,\mathbf{1})$-UXP reduction.

Theorems & Definitions (74)

  • Proposition 1
  • proof
  • Example 1
  • Example 2
  • Example 3
  • Example 4
  • Example 5
  • Example 6
  • Proposition 2
  • Example 7: PA with one variable per inequality
  • ...and 64 more