Document Open Access Logo

An Introduction to the Theory of Linear Integer Arithmetic (Invited Paper)

Author Dmitry Chistikov

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2024.1.pdf
  • Filesize: 1.04 MB
  • 36 pages

Document Identifiers

Author Details

Dmitry Chistikov
  • Centre for Discrete Mathematics and its Applications (DIMAP) &, Department of Computer Science, University of Warwick, UK

Funding

Supported in part by the Engineering and Physical Sciences Research Council [EP/X03027X/1].

Acknowledgements

I would like to thank Christoph Haase for introducing me to arithmetic theories and all my co-authors for sharing inspiration, ideas, and kindness. I am also grateful to Ranko Lazić and Shrisha Rao for useful discussions of the Steinitz lemma and its applications. Last but not least, I would like to thank everyone who gave feedback on early drafts of this paper.

Cite As Get BibTex

Dmitry Chistikov. An Introduction to the Theory of Linear Integer Arithmetic (Invited Paper). In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 1:1-1:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.FSTTCS.2024.1

Abstract

Presburger arithmetic, or linear integer arithmetic (LIA), is a logic that allows one to express linear constraints on integers: equalities, inequalities, and divisibility by nonzero n ∈ ℤ. More formally, it is the first-order theory of integers with addition and ordering. This paper offers a short introduction: what can be expressed in this logical theory, decision problems, and automated reasoning methods.
We begin with an elementary introduction, explaining the language of linear arithmetic constraints by examples. We adopt a theoretical perspective, focusing on the decision problem: determining the truth value of a logical sentence. The following three views on Presburger arithmetic give us three effective methods for decision procedures: a view from geometry (using semi-linear sets), from automata theory (using finite automata and recognizable sets), and from symbolic computation (using quantifier elimination).
The decision problem for existential formulas of Presburger arithmetic is essentially the feasibility problem of integer linear programming. By a fundamental result due to Borosh and Treybig [Proc. Am. Math. Soc. 55(2), 1976] and Papadimitriou [J. ACM 28(4), 1981], it belongs to the complexity class NP. Echoing the three views discussed above, we sketch three proofs of this result and discuss how these ideas have been used and developed in the recent research literature.
This is a companion paper for a conference talk focused on the three views on Presburger arithmetic and their applications. The reader will require background knowledge at the level of undergraduate computer science curricula. The discussion of complexity aspects is more advanced.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Discrete mathematics
  • Theory of computation → Logic
Keywords
  • Logical theories of arithmetic
  • decision procedures

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Roland Meyer, and Mehdi Seyed Salehi. What’s decidable about availability languages? In FSTTCS, pages 192-205, 2015. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2015.192.
  2. Erika Ábrahám, József Kovács, and Anne Remke. SMT: something you must try. In iFM, pages 3-18, 2023. URL: https://doi.org/10.1007/978-3-031-47705-8_1.
  3. Erika Ábrahám and Gereon Kremer. SMT solving for arithmetic theories: Theory and tool support. In SYNASC, pages 1-8, 2017. URL: https://doi.org/10.1109/SYNASC.2017.00009.
  4. Jorge L. Ramírez Alfonsín. Complexity of the Frobenius problem. Combinatorica, 16(1):143-147, 1996. URL: https://doi.org/10.1007/BF01300131.
  5. Jorge L. Ramírez Alfonsín. The Diophantine Frobenius problem. Oxford Lecture Series in Mathematics and Its Applications. Oxford University Press, 2006. URL: https://doi.org/10.1093/acprof:oso/9780198568209.001.0001.
  6. Steven C. Althoen and Renate McLaughlin. Gauss-Jordan reduction: A brief history. Am. Math. Mon., 94(2):130-142, 1987. Google Scholar
  7. Benjamin Assarf, Ewgenij Gawrilow, Katrin Herr, Michael Joswig, Benjamin Lorenz, Andreas Paffenholz, and Thomas Rehn. Computing convex hulls and counting integer points with polymake. Math. Program. Comput., 9(1):1-38, 2017. URL: https://doi.org/10.1007/S12532-016-0104-Z.
  8. Imre Bárány. On the power of linear dependencies. In Building Bridges: Between Mathematics and Computer Science, volume 19 of Bolyai Society Mathematical Studies, pages 31-45. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85221-6_1.
  9. Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In TACAS, pages 415-442, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_24.
  10. Erwin H. Bareiss. Sylvester’s identity and multistep integer-preserving Gaussian elimination. Math. Comput., 22:565-578, 1968. URL: https://doi.org/10.1090/S0025-5718-1968-0226829-0.
  11. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1267-1329. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201017.
  12. Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, and Yoni Zohar. Satisfiability modulo theories: A beginner’s tutorial. In FM, pages 571-596, 2024. URL: https://doi.org/10.1007/978-3-031-71177-0_31.
  13. Alexander Barvinok. Integer points in polyhedra. EMS Press, 2008. URL: https://doi.org/10.4171/052.
  14. Alexander I. Barvinok. A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed. Math. Oper. Res., 19(4):769-779, 1994. URL: https://doi.org/10.1287/MOOR.19.4.769.
  15. Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti. The complexity of Presburger arithmetic with power or powers. In ICALP, pages 112:1-112:18, 2023. URL: https://doi.org/10.4230/LIPICS.ICALP.2023.112.
  16. Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, and Georg Zetzsche. Ramsey quantifiers in linear arithmetics. Proc. ACM Program. Lang., 8(POPL):1-32, 2024. URL: https://doi.org/10.1145/3632843.
  17. Leonard Berman. The complexity of logical theories. Theor. Comput. Sci., 11:71-77, 1980. URL: https://doi.org/10.1016/0304-3975(80)90037-7.
  18. Alexis Bès. A survey of arithmetical definability. A tribute to Maurice Boffa. B. Belg. Math. Soc.-Sim., suppl.:1-54, 2001. URL: http://lacl.u-pec.fr/bes/publi/survey.pdf.
  19. Alexis Bès and Christian Choffrut. Theories of real addition with and without a predicate for integers. Log. Methods Comput. Sci., 17(2), 2021. URL: https://doi.org/10.23638/LMCS-17(2:18)2021.
  20. Nikolaj S. Bjørner and Lev Nachmanson. Arithmetic solving in Z3. In CAV, part I, pages 26-41, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_2.
  21. Bernard Boigelot, Isabelle Mainz, Victor Marsault, and Michel Rigo. An efficient algorithm to decide periodicity of b-recognisable sets using MSDF convention. In ICALP, pages 118:1-118:14, 2017. URL: https://doi.org/10.4230/LIPICS.ICALP.2017.118.
  22. Bernard Boigelot and Pierre Wolper. Representing arithmetic constraints with finite automata: An overview. In ICLP, LNCS, pages 1-19, 2002. URL: https://doi.org/10.1007/3-540-45619-8_1.
  23. George S. Boolos, John P. Burgess, and Richard C. Jeffrey. Computability and Logic. Cambridge University Press, 5th edition, 2007. URL: https://doi.org/10.1017/CBO9780511804076.
  24. Itshak Borosh and Leon Bruce Treybig. Bounds on positive integral solutions of linear Diophantine equations. Proc. Am. Math. Soc., 55(2):299-304, 1976. URL: https://doi.org/10.1090/S0002-9939-1976-0396605-3.
  25. Aaron R. Bradley and Zohar Manna. The calculus of computation: Decision procedures with applications to verification. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74113-8.
  26. Martin Bromberger. Decision Procedures for Linear Arithmetic. PhD thesis, Saarland University, Saarbrücken, Germany, 2019. URL: https://tel.archives-ouvertes.fr/tel-02427371.
  27. Winfried Bruns, Bogdan Ichim, and Christof Söger. The power of pyramid decomposition in Normaliz. J. Symb. Comput., 74:513-536, 2016. URL: https://doi.org/10.1016/J.JSC.2015.09.003.
  28. Winfried Bruns, Bogdan Ichim, Christof Söger, and Ulrich von der Ohe. Normaliz. Algorithms for rational cones and affine monoids. URL: https://www.normaliz.uni-osnabrueck.de/.
  29. Véronique Bruyère, Georges Hansel, Christian Michaux, and Roger Villemaire. Logic and p-recognizable sets of integers. B. Belg. Math. Soc.-Sim., 1(2):191-238, 1994. URL: https://doi.org/10.36045/bbms/1103408547.
  30. J. Richard Büchi. Weak second-order arithmetic and finite automata. Math. Log. Q., 6(1-6):66-92, 1960. URL: https://doi.org/10.1002/malq.19600060105.
  31. Patrick Cegielski, Denis Richard, and Maxim Vsemirnov. On the additive theory of prime numbers II. In CSIT 2005 (Computer Science and Information Technologies, September 19-23, 2005, Yerevan, Armenia), pages 39-47, 2005. URL: https://doi.org/10.48550/arXiv.math/0609554.
  32. Gregory Cherlin and Françoise Point. On extensions of Presburger arithmetic. In 4th Easter Conference on Model Theory, volume 86 of Humboldt-Univ. Berlin Seminarberichte, pages 17-34, 1986. URL: https://webusers.imj-prg.fr/~francoise.point/papiers/cherlin_point86.pdf.
  33. Dmitry Chistikov and Christoph Haase. The taming of the semi-linear set. In ICALP, pages 128:1-128:13, 2016. URL: https://doi.org/10.4230/LIPICS.ICALP.2016.128.
  34. Dmitry Chistikov and Christoph Haase. On the complexity of quantified integer programming. In ICALP, pages 94:1-94:13, 2017. URL: https://doi.org/10.4230/LIPICS.ICALP.2017.94.
  35. Dmitry Chistikov, Christoph Haase, and Alessio Mansutti. Geometric decision procedures and the VC dimension of linear arithmetic theories. In LICS, pages 59:1-59:13, 2022. URL: https://doi.org/10.1145/3531130.3533372.
  36. Dmitry Chistikov, Alessio Mansutti, and Mikhail R. Starchak. Integer linear-exponential programming in NP by quantifier elimination. In ICALP, pages 132:1-132:20, 2024. URL: https://doi.org/10.4230/LIPICS.ICALP.2024.132.
  37. David C. Cooper. Programs for mechanical program verification. In Machine Intelligence, volume 6, pages 43-59. Edinburgh University Press, 1971. Google Scholar
  38. David C. Cooper. Theorem proving in arithmetic without multiplication. In Machine Intelligence, volume 7, pages 91-99. Edinburgh University Press, 1972. Google Scholar
  39. Jesús A. De Loera, Raymond Hemmecke, and Matthias Köppe. Algebraic and geometric ideas in the theory of discrete optimization, volume MO14 of MOS-SIAM Series on Optimization. SIAM and MOS, 2013. URL: https://doi.org/10.1137/1.9781611972443.
  40. Rémy Défossez, Christoph Haase, Alessio Mansutti, and Guillermo A. Pérez. Integer programming with GCD constraints. In SODA, pages 3605-3658, 2024. URL: https://doi.org/10.1137/1.9781611977912.128.
  41. Charles L. Dodgson. Condensation of determinants, being a new and brief method for computing their arithmetical values. Proc. R. Soc. Lond., 15:150-155, 1867. URL: https://doi.org/10.1098/rspl.1866.0037.
  42. Andreas Dolzmann and Thomas Sturm. REDLOG: computer algebra meets computer logic. SIGSAM Bull., 31(2):2-9, 1997. URL: https://doi.org/10.1145/261320.261324.
  43. Andrei Draghici, Christoph Haase, and Florin Manea. Semënov arithmetic, affine VASS, and string constraints. In STACS, pages 29:1-29:19, 2024. URL: https://doi.org/10.4230/LIPICS.STACS.2024.29.
  44. Lou van den Dries. Alfred Tarski’s elimination theory for real closed fields. J. Symb. Log., 53(1):7-19, 1988. URL: https://doi.org/10.1017/S0022481200028899.
  45. Antoine Durand-Gasselin and Peter Habermehl. On the use of non-deterministic automata for Presburger arithmetic. In CONCUR, pages 373-387, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_26.
  46. Antoine Durand-Gasselin and Peter Habermehl. Ehrenfeucht-Fraïssé goes elementarily automatic for structures of bounded degree. In STACS, pages 242-253, 2012. URL: https://doi.org/10.4230/LIPIcs.STACS.2012.242.
  47. Jack Edmonds. Systems of distinct representatives and linear algebra. J. Res. NBS-B. Math. Sci., 71B(4):241-245, 1967. URL: https://doi.org/10.6028/jres.071B.033.
  48. 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.
  49. Friedrich Eisenbrand and Robert Weismantel. Proximity results and faster algorithms for integer programming using the Steinitz lemma. ACM Trans. Algorithms, 16(1):5:1-5:14, 2020. URL: https://doi.org/10.1145/3340322.
  50. Javier Esparza and Michael Blondin. Automata theory: An algorithmic approach. MIT Press, 2023. Google Scholar
  51. Javier Esparza and Pierre Ganty. Complexity of pattern-based verification for multithreaded programs. In POPL, pages 499-510, 2011. URL: https://doi.org/10.1145/1926385.1926443.
  52. Jeanne Ferrante and Charles W. Rackoff. The computational complexity of logical theories, volume 718 of Lecture Notes in Mathematics. Springer, 1979. URL: https://doi.org/10.1007/BFb0062837.
  53. Michael J. Fischer and Michael O. Rabin. Super-exponential complexity of Presburger arithmetic. In Complexity of Computation, volume 7 of SIAM-AMS Proceedings, pages 27-41. AMS, 1974. Google Scholar
  54. Jean Gallier and Jocelyn Quaintance. Aspects of convex geometry: Polyhedra, linear programming, shellings, Voronoi diagrams, Delaunay triangulations, 2022. URL: https://www.cis.upenn.edu/~jean/gbooks/convexpoly.html.
  55. Joachim von zur Gathen and Malte Sieveking. A bound on solutions of linear integer equalities and inequalities. Proc. Am. Math. Soc., 72(1):155-158, 1978. URL: https://doi.org/10.1090/S0002-9939-1978-0500555-0.
  56. Seymour Ginsburg. The mathematical theory of context-free languages. McGraw-Hill, 1966. Google Scholar
  57. Seymour Ginsburg and Edwin H. Spanier. Bounded ALGOL-like languages. Trans. Am. Math. Soc., 113(2):333-368, 1964. URL: https://doi.org/10.1090/S0002-9947-1964-0181500-1.
  58. Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics, 16(2):285-296, 1966. URL: https://doi.org/10.2140/pjm.1966.16.285.
  59. Erich Grädel. Dominoes and the complexity of subclasses of logical theories. Ann. Pure Appl. Log., 43(1):1-30, 1989. URL: https://doi.org/10.1016/0168-0072(89)90023-7.
  60. Erich Grädel. Automatic structures: Twenty years later. In LICS, pages 21-34, 2020. URL: https://doi.org/10.1145/3373718.3394734.
  61. Victor S. Grinberg and Sergey V. Sevast'yanov. Value of the Steinitz constant. Funct. Anal. Appl., 14(2):125-126, 1980. URL: https://doi.org/10.1007/BF01086559.
  62. Florent Guépin, Christoph Haase, and James Worrell. On the existential theories of Büchi arithmetic and linear p-adic fields. In LICS, 2019. URL: https://doi.org/10.1109/LICS.2019.8785681.
  63. Roland Guttenberg, Mikhail A. Raskin, and Javier Esparza. Geometry of reachability sets of vector addition systems. In CONCUR, pages 6:1-6:16, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.6.
  64. Christoph Haase. Subclasses of Presburger arithmetic and the weak EXP hierarchy. In CSL-LICS, pages 47:1-47:10, 2014. URL: https://doi.org/10.1145/2603088.2603092.
  65. Christoph Haase. A survival guide to Presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. URL: https://www.cs.ox.ac.uk/people/christoph.haase/home/publication/haa-18/haa-18.pdf, URL: https://doi.org/10.1145/3242953.3242964.
  66. Christoph Haase. Approaching arithmetic theories with finite-state automata. In LATA, pages 33-43, 2020. URL: https://doi.org/10.1007/978-3-030-40608-0_3.
  67. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in succinct and parametric one-counter automata. In CONCUR, pages 369-383, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_25.
  68. Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, and Georg Zetzsche. An efficient quantifier elimination procedure for Presburger arithmetic. In ICALP, pages 142:1-142:17, 2024. URL: https://doi.org/10.4230/LIPICS.ICALP.2024.142.
  69. Christoph Haase and Georg Zetzsche. Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. In LICS, 2019. URL: https://doi.org/10.1109/LICS.2019.8785850.
  70. Peter Habermehl, Vojtech Havlena, Michal Hecko, Lukás Holík, and Ondrej Lengál. Algebraic reasoning meets automata in solving linear integer arithmetic. In CAV, part I, pages 42-67, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_3.
  71. Peter Habermehl and Dietrich Kuske. On Presburger arithmetic extended with non-unary counting quantifiers. Log. Methods Comput. Sci., 19(3), 2023. URL: https://doi.org/10.46298/LMCS-19(3:4)2023.
  72. Matthew Hague, Artur Jez, and Anthony W. Lin. Parikh’s theorem made symbolic. Proc. ACM Program. Lang., 8(POPL):1945-1977, 2024. URL: https://doi.org/10.1145/3632907.
  73. Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Monadic decomposition in integer linear arithmetic. In IJCAR, pages 122-140, 2020. URL: https://doi.org/10.1007/978-3-030-51074-9_8.
  74. Matthew Hague and Anthony Widjaja Lin. Model checking recursive programs with numeric data types. In CAV, pages 743-759, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_60.
  75. Matthew Hague and Anthony Widjaja Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In CAV, pages 260-276, 2012. Full version: https://anthonywlin.github.io/papers/cav12-long.pdf. URL: https://doi.org/10.1007/978-3-642-31424-7_22.
  76. Jesper G. Henriksen, Jakob L. Jensen, Michael E. Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders Sandholm. Mona: Monadic second-order logic in practice. In TACAS, pages 89-110, 1995. URL: https://doi.org/10.1007/3-540-60630-0_5.
  77. Philipp Hieronymi and Christian Schulz. A strong version of Cobham’s theorem. In STOC, pages 1172-1179, 2022. URL: https://doi.org/10.1145/3519935.3519958.
  78. Thiet-Dung Huynh. The complexity of semilinear sets. Elektron. Inf.verarb. Kybern., 18(6):291-338, 1982. Google Scholar
  79. Petr Janku and Lenka Turonová. Solving string constraints with approximate Parikh image. In EUROCAST (I), volume 12013, pages 491-498, 2019. URL: https://doi.org/10.1007/978-3-030-45093-9_59.
  80. Klaus Jansen and Kim-Manuel Klein. About the structure of the integer cone and its application to bin packing. Math. Oper. Res., 45(4):1498-1511, 2020. URL: https://doi.org/10.1287/MOOR.2019.1040.
  81. Michael Jünger, Thomas M. Liebling, Denis Naddef, George L. Nemhauser, William R. Pulleyblank, Gerhard Reinelt, Giovanni Rinaldi, and Laurence A. Wolsey. 50 years of integer programming 1958-2008: From the early years to the state-of-the-art. Springer, 2009. URL: https://doi.org/10.1007/978-3-540-68279-0.
  82. Anna Karapiperi, Michela Redivo-Zaglia, and Maria Rosaria Russo. Generalizations of Sylvester’s determinantal identity, 2015. URL: https://arxiv.org/abs/1503.00519.
  83. Toghrul Karimov, Florian Luca, Joris Nieuwveld, Joël Ouaknine, and James Worrell. On the decidability of Presburger arithmetic expanded with powers. In SODA, 2025. To appear. URL: https://arxiv.org/abs/2407.05191.
  84. Jonathan Kirby. An invitation to model theory. Cambridge University Press, 2019. URL: https://doi.org/10.1017/9781316683002.
  85. Felix Klaedtke. Bounds on the automata size for Presburger arithmetic. ACM Trans. Comput. Log., 9(2):11:1-11:34, 2008. URL: https://doi.org/10.1145/1342991.1342995.
  86. Nils Klarlund and Anders Møller. MONA Version 1.4 User Manual. BRICS, Department of Computer Science, University of Aarhus, January 2001. Notes Series NS-01-1. URL: http://www.brics.dk/mona/.
  87. Dexter Kozen. Theory of computation. Texts in Computer Science. Springer, 2006. URL: https://doi.org/10.1007/1-84628-477-5.
  88. Georg Kreisel and Jean-Louis Krivine. Elements of mathematical logic (model theory). North Holland, 1967. Google Scholar
  89. Daniel Kroening and Ofer Strichman. Decision procedures: An algorithmic point of view. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2nd edition, 2016. URL: https://doi.org/10.1007/978-3-662-50497-0.
  90. Aless Lasaruk and Thomas Sturm. Weak integer quantifier elimination beyond the linear case. In CASC, pages 275-294, 2007. URL: https://doi.org/10.1007/978-3-540-75187-8_22.
  91. Niels Lauritzen. Lectures on convex sets, 2009. URL: https://users.fmf.uni-lj.si/lavric/lauritzen.pdf.
  92. Niels Lauritzen. Undergraduate convexity: From Fourier and Motzkin to Kuhn and Tucker. World Scientific, 2013. URL: https://doi.org/10.1142/8527.
  93. Thierry Lavendhomme and Arnaud Maes. Note on the undecidability of ⟨ ω; +, P_m,r⟩. In Definability in Arithmetics and Computability, volume 11 of Cahiers du Centre de logique, pages 61-68. Academia-Bruylant, 2000. URL: http://www.cahiersdelogique.be/cahier11angl.html.
  94. Antonia Lechner, Joël Ouaknine, and James Worrell. On the complexity of linear arithmetic with divisibility. In LICS, pages 667-676, 2015. URL: https://doi.org/10.1109/LICS.2015.67.
  95. Hendrik W. Lenstra, Jr. Integer programming with a fixed number of variables. Math. Oper. Res., 8(4):538-548, 1983. URL: https://doi.org/10.1287/MOOR.8.4.538.
  96. Jérôme Leroux. A polynomial time Presburger criterion and synthesis for number decision diagrams. In LICS, pages 147-156, 2005. URL: https://doi.org/10.1109/LICS.2005.2.
  97. Jérôme Leroux. Vector addition system reachability problem: a short self-contained proof. In POPL, pages 307-316, 2011. URL: https://doi.org/10.1145/1926385.1926421.
  98. Jérôme Leroux and Gérald Point. TaPAS: The Talence Presburger arithmetic suite. In TACAS, pages 182-185, 2009. URL: https://doi.org/10.1007/978-3-642-00768-2_18.
  99. Arnaud Maes. Revisiting Semenov’s results about decidability of extensions of Presburger arithmetic. In Definability in Arithmetics and Computability, volume 11 of Cahiers du Centre de logique, pages 11-59. Academia-Bruylant, 2000. URL: http://www.cahiersdelogique.be/cahier11angl.html.
  100. Victor Marsault and Jacques Sakarovitch. Ultimate periodicity of b-recognisable sets: A quasilinear procedure. In DLT, pages 362-373, 2013. URL: https://doi.org/10.1007/978-3-642-38771-5_32.
  101. Jiří Matoušek. Lectures on discrete geometry. Graduate Texts in Mathematics. Springer, 2002. URL: https://doi.org/10.1007/978-1-4613-0039-7.
  102. Jiří Matoušek. Thirty-three miniatures: Mathematical and algorithmic applications of linear algebra, volume 53 of Student Mathematical Library. AMS, 2010. URL: https://doi.org/10.1090/stml/053.
  103. Jirí Matoušek. Intersection graphs of segments and ∃ℝ, 2014. URL: https://arxiv.org/abs/1406.2636.
  104. Christian Michaux and Roger Villemaire. Open questions around Büchi and Presburger arithmetics. In Logic: from Foundations to Applications: European logic colloquium, pages 353-384. Oxford University Press, 1996. URL: https://doi.org/10.1093/oso/9780198538622.003.0015.
  105. Jasper Nalbach, Valentin Promies, Erika Ábrahám, and Paul Kobialka. FMplex: A novel method for solving linear real arithmetic problems. In GandALF, pages 16-32, 2023. URL: https://doi.org/10.4204/EPTCS.390.2.
  106. Danny Nguyen and Igor Pak. Enumerating projections of integer points in unbounded polyhedra. SIAM J. Discret. Math., 32(2):986-1002, 2018. URL: https://doi.org/10.1137/17M1118907.
  107. Danny Nguyen and Igor Pak. Short Presburger arithmetic is hard. SIAM J. Comput., 51(2):1-31, 2022. URL: https://doi.org/10.1137/17M1151146.
  108. Phong Q. Nguyen and Brigitte Vallée, editors. The LLL algorithm: Survey and applications. Information Security and Cryptography. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-02295-1.
  109. Tobias Nipkow. Linear quantifier elimination. J. Autom. Reason., 45(2):189-212, 2010. URL: https://doi.org/10.1007/S10817-010-9183-0.
  110. Timm Oertel, Joseph Paat, and Robert Weismantel. A colorful Steinitz lemma with application to block-structured integer programs. Math. Program., 204(1):677-702, 2024. URL: https://doi.org/10.1007/S10107-023-01971-3.
  111. Derek C. Oppen. A 2^2^2^pn upper bound on the complexity of Presburger arithmetic. J. Comput. Syst. Sci., 16(3):323-332, 1978. URL: https://doi.org/10.1016/0022-0000(78)90021-1.
  112. Andreas Paffenholz. Polyhedral geometry and linear optimization (summer semester 2010), 2013. URL: http://www.mathematik.tu-darmstadt.de/~paffenholz/data/preprints/geometry_of_optimization.pdf.
  113. Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765-768, 1981. URL: https://doi.org/10.1145/322276.322287.
  114. Rohit Parikh. On context-free languages. J. ACM, 13(4):570-581, 1966. URL: https://doi.org/10.1145/321356.321364.
  115. Hector Pasten. Definability and arithmetic. Notices of the AMS, 70(9):1385-1393, 2023. URL: https://doi.org/10.1090/noti2777.
  116. Guillermo A. Pérez and Ritam Raha. Revisiting parameter synthesis for one-counter automata. In CSL, pages 33:1-33:18, 2022. URL: https://doi.org/10.4230/LIPICS.CSL.2022.33.
  117. Jean-Éric Pin, editor. Handbook of automata theory. Volume II. Automata in mathematics and selected applications. EMS Press, 2021. URL: https://doi.org/10.4171/AUTOMATA-2.
  118. Ruzica Piskac and Viktor Kuncak. Linear arithmetic with stars. In CAV, pages 268-280, 2008. URL: https://doi.org/10.1007/978-3-540-70545-1_25.
  119. Françoise Point. On the expansion (ℕ;+,2^x) of Presburger arithmetic, 2007. Preprint. URL: https://webusers.imj-prg.fr/~francoise.point/papiers/Pres.pdf.
  120. Bjorn Poonen. Hilbert’s Tenth Problem over rings of number-theoretic interest. Notes from the lectures at the Arizona Winter School "Logic and Number Theory", 2003. URL: http://math.mit.edu/~poonen/papers/aws2003.pdf.
  121. Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du I Congrès des Mathématiciens des Pays Slaves, Varsovie, 1929, pages 92-101. Skład Główny, 1930. Google Scholar
  122. Mojżesz Presburger and Dale Jabcquette. On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation. History and Philosophy of Logic, 12(2):225-233, 1991. Translation of ref. [Mojżesz Presburger, 1930] and commentary. URL: https://doi.org/10.1080/014453409108837187.
  123. William W. Pugh. A practical algorithm for exact array dependence analysis. Commun. ACM, 35(8):102-114, 1992. URL: https://doi.org/10.1145/135226.135233.
  124. Andrew Reynolds, Tim King, and Viktor Kuncak. Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des., 51(3):500-532, 2017. URL: https://doi.org/10.1007/S10703-017-0290-Y.
  125. Michel Rigo. Numeration systems: A link between number theory and formal language theory. In DLT, pages 33-53, 2010. URL: https://doi.org/10.1007/978-3-642-14455-4_6.
  126. Julia Robinson. Definability and decision problems in arithmetic. J. Symb. Log., 14(2):98-114, 1949. URL: https://doi.org/10.2307/2266510.
  127. R. Tyrrell Rockafellar. Convex analysis. Princeton University Press, 1970. URL: https://doi.org/10.1515/9781400873173.
  128. Bruno Scarpellini. Complexity of subcases of Presburger arithmetic. Trans. Am. Math. Soc., 284(1):203-218, 1984. URL: https://doi.org/10.1090/S0002-9947-1984-0742421-9.
  129. Alexander Schrijver. Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization. Wiley, 1999. Google Scholar
  130. Nicole Schweikardt. Arithmetic, first-order logic, and counting quantifiers. ACM Trans. Comput. Log., 6(3):634-671, 2005. URL: https://doi.org/10.1145/1071596.1071602.
  131. Helmut Seidl, Thomas Schwentick, Anca Muscholl, and Peter Habermehl. Counting in trees for free. In ICALP, pages 1136-1149, 2004. URL: https://doi.org/10.1007/978-3-540-27836-8_94.
  132. Aleksei L. Semenov. On certain extensions of the arithmetic of addition of natural numbers. Math. USSR Izv., 15(2):401-418, 1980. URL: https://doi.org/10.1070/IM1980v015n02ABEH001252.
  133. Aleksei L. Semenov. Logical theories of one-place functions on the set of natural numbers. Math. USSR Izv., 22(3):587-618, 1984. URL: https://doi.org/10.1070/IM1984v022n03ABEH001456.
  134. Jeffrey Shallit. The logical approach to automatic sequences: Exploring combinatorics on words with Walnut, volume 482 of London Mathematical Society Lecture Note Series. Cambridge University Press, 2022. URL: https://doi.org/10.1017/9781108775267.
  135. Alexander Shen and Nikolay K. Vereshchagin. Computable functions, volume 19 of Student Mathematical Library. AMS, 2003. URL: https://doi.org/10.1090/stml/019.
  136. Michael Sipser. Introduction to the theory of computation. Cengage Learning, 2013. 3rd ed. Google Scholar
  137. Ryan Stansifer. Presburger’s article on integer arithmetic: Remarks and translation. Technical Report TR 84-639, Department of Computer Science, Cornell University, Ithaca, New York, September 1984. URL: https://hdl.handle.net/1813/6478.
  138. Mikhail R. Starchak. Positive existential definability with unit, addition and coprimeness. In ISSAC, pages 353-360, 2021. URL: https://doi.org/10.1145/3452143.3465515.
  139. Mikhail R. Starchak. On the existential arithmetics with addition and bitwise minimum. In FoSSaCS, pages 176-195, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_9.
  140. Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. On the complexity of equational Horn clauses. In CADE, pages 337-352, 2005. URL: https://doi.org/10.1007/11532231_25.
  141. Volker Weispfenning. The complexity of almost linear diophantine problems. J. Symb. Comput., 10(5):395-404, 1990. URL: https://doi.org/10.1016/S0747-7171(08)80051-X.
  142. Volker Weispfenning. Complexity and uniformity of elimination in Presburger arithmetic. In ISSAC, pages 48-53, 1997. URL: https://doi.org/10.1145/258726.258746.
  143. Volker Weispfenning. Mixed real-integer linear quantifier elimination. In ISSAC, pages 129-136, 1999. URL: https://doi.org/10.1145/309831.309888.
  144. Herbert S. Wilf. A circle-of-lights algorithm for the "money-changing problem". Am. Math. Mon., 85(7):562-565, 1978. URL: https://doi.org/10.2307/2320864.
  145. H. Paul Williams. Logic and integer programming, volume 130 of International Series in Operations Research & Management Science. Springer, 2009. URL: https://doi.org/10.1007/978-0-387-92280-5.
  146. Hao Wu, Yu-Fang Chen, Zhilin Wu, Bican Xia, and Naijun Zhan. A decision procedure for string constraints with string/integer conversion and flat regular constraints. Acta Inform., 61(1):23-52, 2024. URL: https://doi.org/10.1007/S00236-023-00446-4.
  147. Dennis Yurichev. SAT/SMT by example. Version of May 12, 2024. URL: https://smt.st/.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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