2026-08-03T22:50:46Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18586 2024-03-06T11:02:11Z ddc:004 open_access

On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract) Haase, Christoph Mansutti, Alessio Pouly, Amaury first-order theories arithmetic theories fixed-parameter tractability 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christoph Haase and Alessio Mansutti and Amaury Pouly 2023 Is Part Of LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2023.52 urn:nbn:de:0030-drops-185869 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.52 eng https://creativecommons.org/licenses/by/4.0/legalcode