TY - GEN
T1 - On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract)
AU - Pouly, Amaury
AU - Haase, Christoph
AU - Mansutti, Alessio
N1 - Publisher Copyright:
© Christoph Haase, Alessio Mansutti, and Amaury Pouly;
PY - 2023/8/1
Y1 - 2023/8/1
N2 - 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.
AB - 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.
KW - arithmetic theories
KW - first-order theories
KW - fixed-parameter tractability
UR - https://www.scopus.com/pages/publications/85171463030
U2 - 10.4230/LIPIcs.MFCS.2023.52
DO - 10.4230/LIPIcs.MFCS.2023.52
M3 - Conference contribution
AN - SCOPUS:85171463030
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023
A2 - Leroux, Jerome
A2 - Lombardy, Sylvain
A2 - Peleg, David
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023
Y2 - 28 August 2023 through 1 September 2023
ER -