{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T10:08:20Z","timestamp":1790676500185,"version":"4.1.0"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2018,7,26]],"date-time":"2018-07-26T00:00:00Z","timestamp":1532563200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM SIGLOG News"],"published-print":{"date-parts":[[2018,7,26]]},"abstract":"<jats:p>The first-order theory of the integers with addition and order, commonly known as Presburger arithmetic, has been a central topic in mathematical logic and computer science for almost 90 years. Presburger arithmetic has been the starting point for numerous lines of research in automata theory, model theory and discrete geometry. In formal verification, Presburger arithmetic is the first-choice logic to represent and reason about systems with infinitely many states. This article provides a broad yet concise overview over the history, decision procedures, extensions and geometric properties of Presburger arithmetic.<\/jats:p>","DOI":"10.1145\/3242953.3242964","type":"journal-article","created":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T05:28:34Z","timestamp":1585978114000},"page":"67-82","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":64,"title":["A survival guide to presburger arithmetic"],"prefix":"10.1145","volume":"5","author":[{"given":"Christoph","family":"Haase","sequence":"first","affiliation":[{"name":"University of Oxford, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,7,26]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1287\/moor.19.4.769"},{"key":"e_1_2_1_2_1","first-page":"41","article-title":"On the Descriptional Complexity of Operations on Semilinear Sets","volume":"252","author":"Beier Simon","year":"2017","journal-title":"Automata and Formal Languages (AFL) (EPTCS)"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90037-7"},{"key":"e_1_2_1_4_1","unstructured":"Alexis B\u00e8s. 2002. A survey of arithmetical definability. In A tribute to Maurice Boffa. Soci\u00e9t\u00e9 Math\u00e9matique de Belgique 1--54.  Alexis B\u00e8s. 2002. A survey of arithmetical definability. In A tribute to Maurice Boffa. Soci\u00e9t\u00e9 Math\u00e9matique de Belgique 1--54."},{"key":"e_1_2_1_5_1","unstructured":"Michael Blondin. 2018. Personal communication. (2018).  Michael Blondin. 2018. Personal communication. (2018)."},{"key":"e_1_2_1_6_1","volume-title":"Logic in Computer Science (LICS)","author":"Blumensath Achim"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1976-0396605-3"},{"key":"e_1_2_1_8_1","volume-title":"Trees in Algebra and Programming (CAAP) (Lect. Notes Comp. Sci.)","author":"Boudet Alexandre"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.36045\/bbms\/1103408547"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19600060105"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_2_1_12_1","volume-title":"Automata, Languages, and Programming (ICALP) (LIPIcs)","author":"Chistikov Dmitry"},{"key":"e_1_2_1_13_1","volume-title":"Automata, Languages, and Programming (ICALP) (LIPIcs)","author":"Chistikov Dmitry"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.06.017"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.2307\/2371045"},{"key":"e_1_2_1_16_1","first-page":"91","article-title":"Theorem proving in arithmetic without multiplication","volume":"7","author":"Cooper David C.","year":"1972","journal-title":"Mach. Intell."},{"key":"e_1_2_1_17_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, TACAS (Lect. Notes Comp. Sci.)","author":"de Moura Leonardo Mendon\u00e7a"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_2_1_19_1","volume-title":"Concurrency Theory (CONCUR) (Lect. Notes Comp. Sci.)","author":"Durand-Gasselin Antoine"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0021-8693(69)90070-2"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.orl.2005.09.008"},{"key":"e_1_2_1_22_1","unstructured":"Herbert B. Enderton. 1972. A mathematical introduction to logic. Academic Press.  Herbert B. Enderton. 1972. A mathematical introduction to logic. Academic Press."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1137\/0204006"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Michael J. Fischer and Michael O. Rabin. 1998. Super-Exponential Complexity of Presburger Arithmetic. In Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Vienna 122--135.  Michael J. Fischer and Michael O. Rabin. 1998. Super-Exponential Complexity of Presburger Arithmetic. In Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Vienna 122--135.","DOI":"10.1007\/978-3-7091-9459-1_5"},{"key":"e_1_2_1_25_1","unstructured":"Jean Baptiste Joseph Fourier. 1826. Solution d'une question particuliere du calcul des in\u00e9galit\u00e9s. Nouveau Bulletin des Sciences par la Soci\u00e9t\u00e9 philomatique de Paris 99 (1826) 100.  Jean Baptiste Joseph Fourier. 1826. Solution d'une question particuliere du calcul des in\u00e9galit\u00e9s. Nouveau Bulletin des Sciences par la Soci\u00e9t\u00e9 philomatique de Paris 99 (1826) 100."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02579200"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Seymor Ginsburg and Edwin H. Spanier. 1964. Bounded ALGOL-like languages. T. Am. Math. Soc. (1964) 333--368.  Seymor Ginsburg and Edwin H. Spanier. 1964. Bounded ALGOL-like languages. T. Am. Math. Soc. (1964) 333--368.","DOI":"10.1090\/S0002-9947-1964-0181500-1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90136-3"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/322139.322152"},{"key":"e_1_2_1_30_1","unstructured":"Christoph Haase. 2012. On the Complexity of Model Checking Counter Automata. Ph.D. Dissertation. University of Oxford.  Christoph Haase. 2012. On the Complexity of Model Checking Counter Automata. Ph.D. Dissertation. University of Oxford."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603092"},{"key":"e_1_2_1_32_1","volume-title":"Foundations of Software Science and Computation Structures (FoSSaCS) (Lect. Notes Comp. Sci.)","author":"Habermehl Peter"},{"key":"e_1_2_1_33_1","unstructured":"David Hilbert and Wilhelm Ackermann. 1950. Principles of Mathematical Logic. Chelsea Pub. Co.  David Hilbert and Wilhelm Ackermann. 1950. Principles of Mathematical Logic. Chelsea Pub. Co."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90042-1"},{"key":"e_1_2_1_35_1","first-page":"147","article-title":"A Simple Proof for the \u03a3<sup>p<\/sup><sub>2<\/sub> Upper Bound of the Inequivalence Problem for Semilinear Sets","volume":"22","author":"Huynh Dung T.","year":"1986","journal-title":"Elektron. Inf.verarb. Kybern."},{"key":"e_1_2_1_36_1","first-page":"291","article-title":"The Complexity of Semilinear Sets","volume":"18","author":"Huynh Thiet-Dung","year":"1982","journal-title":"Elektron. Inf.verarb. Kybern."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80014-0"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Gareth A. Jones and J. Mary Jones Jones. 1998. Elementary Number Theory. Springer London.  Gareth A. Jones and J. Mary Jones Jones. 1998. Elementary Number Theory. Springer London.","DOI":"10.1007\/978-1-4471-0613-5"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01204720"},{"key":"e_1_2_1_40_1","volume-title":"Logical and Computational Complexity (Lect. Notes Comp. Sci.)","author":"Khoussainov Bakhadyr"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1342991.1342995"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.21"},{"key":"e_1_2_1_43_1","unstructured":"Dexter Kozen. 2006. Theory of Computation. Springer.   Dexter Kozen. 2006. Theory of Computation. Springer."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.67"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1287\/moor.8.4.538"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1978-0469886-1"},{"key":"e_1_2_1_47_1","volume-title":"Proc. Model Theory Meeting","volume":"33","author":"Lipshitz Leonard M.","year":"1981"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/800113.803627"},{"key":"e_1_2_1_49_1","volume-title":"Foundations of Computer Science (FOCS)","author":"Nguyen Danny"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90021-1"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/321356.321364"},{"key":"e_1_2_1_52_1","first-page":"162","article-title":"Minimal solutions of linear Diophantine systems : bounds and algorithms. In Rewriting Techniques and Applications (RTA). Lect. Notes","volume":"488","author":"Pottier Lo\u00efc","year":"1991","journal-title":"Comp. Sci."},{"key":"e_1_2_1_53_1","unstructured":"Moj\u017cesz Presburger. 1929. \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du I congres de Mathematiciens des Pays Slaves. 92--101.  Moj\u017cesz Presburger. 1929. \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du I congres de Mathematiciens des Pays Slaves . 92--101."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266510"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1984-0742421-9"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02679468"},{"key":"e_1_2_1_57_1","unstructured":"Alexander Schrijver. 1986. Theory of linear and integer programming. John Wiley & Sons.   Alexander Schrijver. 1986. Theory of linear and integer programming . John Wiley & Sons."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1071596.1071602"},{"key":"e_1_2_1_59_1","volume-title":"On the Containment Problem for Linear Sets. In Symposium on Theoretical Aspects of Computer Science (STACS) (LIPIcs)","volume":"96","author":"Simon Hans Ulrich","year":"2018"},{"key":"e_1_2_1_60_1","doi-asserted-by":"crossref","unstructured":"Craig Smory\u0144ski. 1991. Logical number theory I: An introduction. Springer.  Craig Smory\u0144ski. 1991. Logical number theory I: An introduction . Springer.","DOI":"10.1007\/978-3-642-75462-3"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90256-F"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1978-0500555-0"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(08)80051-X"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1986.11971923"},{"key":"e_1_2_1_65_1","volume-title":"Static Analysis (SAS) (Lect. Notes Comp. Sci.)","author":"Wolper Pierre"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2015.4"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1080\/014453409108837186"}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3242953.3242964","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3242953.3242964","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:39:24Z","timestamp":1750196364000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3242953.3242964"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,26]]},"references-count":67,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,7,26]]}},"alternative-id":["10.1145\/3242953.3242964"],"URL":"https:\/\/doi.org\/10.1145\/3242953.3242964","relation":{},"ISSN":["2372-3491"],"issn-type":[{"value":"2372-3491","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,26]]},"assertion":[{"value":"2018-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}