On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908876679413760 |
|---|---|
| author | Haase, Christoph Mansutti, Alessio Pouly, Amaury |
| author_facet | Haase, Christoph Mansutti, Alessio Pouly, Amaury |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_18420 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories Haase, Christoph Mansutti, Alessio Pouly, Amaury Logic in Computer Science 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. |
| title | On Polynomial-Time Decidability of k-Negations Fragments of First-Order Theories |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2407.18420 |