Document Open Access Logo

Analysis of Logics with Arithmetic

Authors Michael Benedikt , Chia-Hsuan Lu , Tony Tan

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.27.pdf
  • Filesize: 0.96 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Presburger quantifiers
  • Spectrum
  • Guarded logics

Metrics

Abstract

We present new results on finite satisfiability of logics with counting and arithmetic. One result is a tight bound on the complexity of satisfiability of logics with so-called local Presburger quantifiers, which sum over neighbors of a node in a graph. A second contribution concerns computing a semilinear representation of the cardinalities associated with a formula in two variable logic extended with counting quantifiers. Such a representation allows you to get bounds not only on satisfiability for these logics, but for satisfiability in the presence of additional "global cardinality constraints": restrictions on cardinalities of unary formulas, expressed using arbitrary decidability logics over arithmetic. In the process, we provide simpler proofs of some key prior results on finite satisfiability and semi-linearity of the spectrum for these logics.

Cite As Get BibTex

Michael Benedikt, Chia-Hsuan Lu, and Tony Tan. Analysis of Logics with Arithmetic. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.27

Author Details

Michael Benedikt
  • University of Oxford, UK
Chia-Hsuan Lu
  • University of Oxford, UK
Tony Tan
  • University of Liverpool, UK

References

  1. Franz Baader. Expressive cardinality restrictions on concepts in a description logic with expressive number restrictions. SIGAPP Appl. Comput. Rev., 19(3), 2019. Google Scholar
  2. Bartosz Bednarczyk. One-variable logic meets presburger arithmetic. Theoretical Computer Science, 802:141-146, 2020. URL: https://doi.org/10.1016/J.TCS.2019.09.028.
  3. Bartosz Bednarczyk and Oskar Fiuk. Presburger büchi tree automata with applications to logics with expressive counting. In Logic, Language, Information, and Computation, pages 295-308, Cham, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-031-15298-6_19.
  4. Bartosz Bednarczyk, Maja Orlowska, Anna Pacanowska, and Tony Tan. On classical decidable logics extended with percentage quantifiers and arithmetics. In FSTTCS, 2021. Google Scholar
  5. Michael Benedikt, Egor Kostylev, and Tony Tan. Two Variable Logic with Ultimately Periodic Counting. SIAM Journal on Computing, 53(4):884-968, 2024. URL: https://doi.org/10.1137/22M1504792.
  6. Michael Benedikt, Chia-Hsuan Liu, Boris Motik, and Tony Tan. Verification of graph neural networks via logical characterizations. In ICALP, 2024. Google Scholar
  7. Friedrich Eisenbrand and Gennady Shmonin. Carathéodory bounds for integer cones. Oper. Res. Lett., 34(5):564-568, 2006. URL: https://doi.org/10.1016/J.ORL.2005.09.008.
  8. Christoph Haase and Georg Zetzsche. Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. In LICS, 2019. Google Scholar
  9. Narendra Karmarkar. A new polynomial-time algorithm for linear programming. In STOC, 1984. Google Scholar
  10. Yevgeny Kazakov. A polynomial translation from the two-variable guarded fragment with number restrictions to the guarded fragment. In JELIA, 2004. Google Scholar
  11. Eryk Kopczynski and Tony Tan. Regular graphs and the spectra of two-variable logic with counting. SIAM J. Comput., 44(3):786-818, 2015. URL: https://doi.org/10.1137/130943625.
  12. Chia-Hsuan Lu and Tony Tan. On two-variable guarded fragment logic with expressive local Presburger constraints. Logical Methods in Computer Science, 20, 2024. URL: https://doi.org/10.46298/LMCS-20(3:16)2024.
  13. Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765-768, 1981. URL: https://doi.org/10.1145/322276.322287.
  14. Rohit Parikh. On Context-Free Languages. JACM, 13(4):570-581, 1966. URL: https://doi.org/10.1145/321356.321364.
  15. Ian Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. Journal of Logic Language and Information, 14:369-395, 2005. URL: https://doi.org/10.1007/S10849-005-5791-1.
  16. Ian Pratt-Hartmann. Complexity of the guarded two-variable fragment with counting quantifiers. Journal of Logic and Computation, 17(1):133-155, 2007. URL: https://doi.org/10.1093/LOGCOM/EXL034.
  17. Ian Pratt-Hartmann. The two-variable fragment with counting. In WoLLIC, 2010. Google Scholar
  18. "Johann" Sebastian Rudolph. Presburger concept cardinality constraints in very expressive description logics - allegro sexagenarioso ma non ritardando. In Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 2019. URL: https://doi.org/10.1007/978-3-030-22102-7_25.
  19. Aleksei L. Semenov. Logical theories of one-place functions on the set of natural numbers. Math. USSR Izv., 22(3):587-618, 1984. Google Scholar
  20. Boris Trakhtenbrot. The Impossibility of an Algorithm for the Decidability Problem on Finite Classes. Proceedings of the USSR Academy of Sciences, 70(4):569-572, 1950. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact