{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,27]],"date-time":"2026-07-27T20:05:32Z","timestamp":1785182732941,"version":"3.55.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032014740","type":"print"},{"value":"9783032014757","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,8,17]],"date-time":"2025-08-17T00:00:00Z","timestamp":1755388800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,17]],"date-time":"2025-08-17T00:00:00Z","timestamp":1755388800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-01475-7_1","type":"book-chapter","created":{"date-parts":[[2025,8,16]],"date-time":"2025-08-16T17:39:21Z","timestamp":1755365961000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Languages and\u00a0Arithmetic Theories: Recent Results and\u00a0Open Problems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5452-936X","authenticated-orcid":false,"given":"Christoph","family":"Haase","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2288-9483","authenticated-orcid":false,"given":"Mikhail","family":"Starchak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,8,17]]},"reference":[{"key":"1_CR1","unstructured":"Belyanin, G., Frolov, T., Starchak, M.: ChrobELIAS: chrobak normal form-based exponential linear integer arithmetic solver (2025). https:\/\/github.com\/Chrobelias\/Chrobelias. Accessed 8 June 2025"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Benedikt, M., Chistikov, D., Mansutti, A.: The complexity of Presburger arithmetic with power or powers. In: Proceedings of the ICALP. Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0261, pp. 112:1\u2013112:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2023.112","DOI":"10.4230\/LIPIcs.ICALP.2023.112"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Berzish, M., et al.: Towards more efficient methods for solving regular-expression heavy string constraints. Theor. Comput. Sci. 943, 50\u201372 (2023). https:\/\/doi.org\/10.1016\/j.tcs.2022.12.009","DOI":"10.1016\/j.tcs.2022.12.009"},{"issue":"4","key":"1_CR4","doi-asserted-by":"publisher","first-page":"1280","DOI":"10.2307\/2275643","volume":"62","author":"A B\u00e8s","year":"1997","unstructured":"B\u00e8s, A.: Undecidable extensions of B\u00fcchi arithmetic and Cobham-Sem\u00ebnov theorem. J. Symb. Log. 62(4), 1280\u20131296 (1997). https:\/\/doi.org\/10.2307\/2275643","journal-title":"J. Symb. Log."},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Boigelot, B., Fontaine, P., Vergain, B.: Universal first-order quantification over automata. In: Proceedings of the CIAA. LNCS, vol. 14151, pp. 91\u2013102. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-40247-0_6","DOI":"10.1007\/978-3-031-40247-0_6"},{"issue":"2","key":"1_CR6","doi-asserted-by":"publisher","first-page":"299","DOI":"10.2307\/2041711","volume":"55","author":"I Borosh","year":"1976","unstructured":"Borosh, I., Treybig, L.B.: Bounds on positive integral solutions of linear Diophantine equations. Proc. Am. Math. Soc. 55(2), 299\u2013304 (1976). https:\/\/doi.org\/10.2307\/2041711","journal-title":"Proc. Am. Math. Soc."},{"key":"1_CR7","unstructured":"Bruy\u00e8re, V.: Entiers et automates finis. M\u00e9moire de fin d\u2019\u00e9tudes (1985)"},{"key":"1_CR8","doi-asserted-by":"publisher","unstructured":"Bruy\u00e8re, V., Hansel, G., Michaux, C., Villemaire, R.: Logic and $$p$$-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin 1(2), 191\u2013238 (1994). https:\/\/doi.org\/10.36045\/bbms\/1103408547","DOI":"10.36045\/bbms\/1103408547"},{"issue":"1\u20136","key":"1_CR9","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"RJ B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, R.J.: Weak second-order arithmetic and finite automata. Math. Logic Quart. 6(1\u20136), 66\u201392 (1960). https:\/\/doi.org\/10.1002\/malq.19600060105","journal-title":"Math. Logic Quart."},{"key":"1_CR10","unstructured":"B\u00fcchi, R.J.: On a decision method in restricted second order arithmetic. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Logic, methodology and philosophy of science, Proceedings of the 1960 International Congress, pp. 1\u201311. Stanford University Press, Stanford, Calif (1962)"},{"key":"1_CR11","unstructured":"Cherlin, G., Point, F.: On extensions of Presburger arithmetic. In: Proceedings of the fourth Easter conference on model theory in Gro\u00df K\u00f6ris, pp. 17\u201334. Seminarberichte 86, Humboldt University, Berlin, Gro\u00df K\u00f6ris, Germany (1986)"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Chistikov, D., Haase, C.: On the complexity of quantified integer programming. In: Proceedings of the ICALP. LIPIcs, vol.\u00a080, pp. 94:1\u201394:13. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017). https:\/\/doi.org\/10.4230\/LIPICS.ICALP.2017.94","DOI":"10.4230\/LIPICS.ICALP.2017.94"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Chistikov, D., Mansutti, A., Starchak, M.R.: Integer linear-exponential programming in NP by quantifier elimination. In: Proceedings of the ICALP. LIPIcs, vol.\u00a0297, pp. 132:1\u2013132:20 (2024). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2024.132","DOI":"10.4230\/LIPIcs.ICALP.2024.132"},{"issue":"1","key":"1_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0168-0072(90)90080-L","volume":"48","author":"KJ Compton","year":"1990","unstructured":"Compton, K.J., Henson, C.W.: A uniform method for proving lower bounds on the computational complexity of logical theories. Ann. Pure Appl. Logic 48(1), 1\u201379 (1990). https:\/\/doi.org\/10.1016\/0168-0072(90)90080-L","journal-title":"Ann. Pure Appl. Logic"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Draghici, A., Haase, C., Manea, F.: Sem\u00ebnov arithmetic, affine VASS, and string constraints. In: Proceedings of the STACS, pp. 29:1\u201329:19. Leibniz International Proceedings in Informatics (LIPIcs) (2024). https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2024.29","DOI":"10.4230\/LIPIcs.STACS.2024.29"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Durand-Gasselin, A., Habermehl, P.: Ehrenfeucht-fra\u00efss\u00e9 goes elementarily automatic for structures of bounded degree. In: Proceedings of the STACS. LIPIcs, vol.\u00a014, pp. 242\u2013253. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012). https:\/\/doi.org\/10.4230\/LIPICS.STACS.2012.242","DOI":"10.4230\/LIPICS.STACS.2012.242"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Satisfiability modulo exponential integer arithmetic. In: Proceedings of the IJCAR, pp. 344\u2013365. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_21","DOI":"10.1007\/978-3-031-63498-7_21"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"von\u00a0zur Gathen, J., Sieveking, M.: A bound on solutions of linear integer equalities and inequalities. Proc. Am. Math. Soc. (1978). https:\/\/doi.org\/10.1090\/S0002-9939-1978-0500555-0","DOI":"10.1090\/S0002-9939-1978-0500555-0"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Gu\u00e9pin, F., Haase, C., Worrell, J.: On the existential theories of B\u00fcchi arithmetic and linear $$p$$-Adic fields. In: Proceedings of the LICS, pp. 1\u201310 (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785681","DOI":"10.1109\/LICS.2019.8785681"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Haase, C., Pi\u00f3rkowski, R.: Universal quantification makes automatic structures hard to decide. In: Proceedings of the CONCUR 2023. LIPIcs, vol.\u00a0279, pp. 13:1\u201313:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2023.13","DOI":"10.4230\/LIPICS.CONCUR.2023.13"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Haase, C., Pi\u00f3rkowski, R.: Universal quantification makes automatic structures hard to decide. CoRR (2024https:\/\/doi.org\/10.48550\/ARXIV.2306.10432","DOI":"10.48550\/ARXIV.2306.10432"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Haase, C., R\u00f3\u017cycki, J.: On the expressiveness of B\u00fcchi arithmetic. Presented at the (2021). https:\/\/doi.org\/10.1007\/978-3-030-71995-1_16","DOI":"10.1007\/978-3-030-71995-1_16"},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Hashiguchi, K.: Representation theorems on regular languages. J. Comput. Syst. Sci. 27(1), 101\u2013115 (1983). https:\/\/doi.org\/10.1016\/0022-0000(83)90031-4","DOI":"10.1016\/0022-0000(83)90031-4"},{"issue":"3","key":"1_CR24","doi-asserted-by":"publisher","first-page":"818","DOI":"10.2307\/2274135","volume":"49","author":"JP Jones","year":"1984","unstructured":"Jones, J.P., Matijasevich, Y.V.: Register machine proof of the theorem on exponential diophantine representation of enumerable sets. J. Symb. Log. 49(3), 818\u2013829 (1984). https:\/\/doi.org\/10.2307\/2274135","journal-title":"J. Symb. Log."},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Matiyasevich, Yu.V.: A new proof of the theorem on exponential diophantine representation of enumerable sets (in Russian). Zapiski Nauchnykh Seminarov LOMI 60, 75\u201392 (1976). https:\/\/doi.org\/10.1007\/BF01693980, English translation: J. Soviet Math. 14(5), 1475\u20131486 (1980)","DOI":"10.1007\/BF01693980"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"McNaughton, R.: Review of [9] and [10]. J. Symb. Log. 28(1), 100\u2013102 (1963). https:\/\/doi.org\/10.2307\/2271342","DOI":"10.2307\/2271342"},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"Meyer, A.R.: Weak monadic second order theory of succesor is not elementary-recursive. In: Logic Colloquium. Lecture Notes in Mathematics, vol.\u00a0453, pp. 132\u2013154. Springer Berlin Heidelberg (1975https:\/\/doi.org\/10.1007\/BFb0064872","DOI":"10.1007\/BFb0064872"},{"issue":"1","key":"1_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(02)00847-2","volume":"304","author":"A Muchnik","year":"2003","unstructured":"Muchnik, A., Semenov, A., Ushakov, M.: Almost periodic sequences. Theor. Comput. Sci. 304(1), 1\u201333 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(02)00847-2","journal-title":"Theor. Comput. Sci."},{"key":"1_CR29","unstructured":"Point, F.: On the expansion of $$(\\mathbb{N},+,2^x)$$ of Presburger arithmetic (2010). https:\/\/u.osu.edu\/friedman.8\/files\/2014\/01\/0AppB072710-1mnlwyn.pdf, unpublished manuscript"},{"issue":"2","key":"1_CR30","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1070\/im1980v015n02abeh001252","volume":"15","author":"AL Sem\u00ebnov","year":"1980","unstructured":"Sem\u00ebnov, A.L.: On certain extensions of the arithmetic of addition of natural numbers. Math. USSR-Izvestiya 15(2), 401\u2013418 (1980). https:\/\/doi.org\/10.1070\/im1980v015n02abeh001252","journal-title":"Math. USSR-Izvestiya"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Sem\u00ebnov, A.L.: Logical theories of one-place functions on integers. Habilitation Thesis (1984)","DOI":"10.1070\/IM1984v022n03ABEH001456"},{"issue":"3","key":"1_CR32","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1070\/im1984v022n03abeh001456","volume":"22","author":"AL Sem\u00ebnov","year":"1984","unstructured":"Sem\u00ebnov, A.L.: Logical theories of one-place functions on the set of natural numbers. Math. USSR-Izvestiya 22(3), 587\u2013618 (1984). https:\/\/doi.org\/10.1070\/im1984v022n03abeh001456","journal-title":"Math. USSR-Izvestiya"},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"Starchak, M.R.: On the existential arithmetics with addition and bitwise minimum. In: Proc. FoSSaCS. LNCS, vol. 13992, pp. 176\u2013195. Springer International Publishing (2023). https:\/\/doi.org\/10.1007\/978-3-031-30829-1_9","DOI":"10.1007\/978-3-031-30829-1_9"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Starchak, M.R.: Existential definability of unary predicates in B\u00fcchi arithmetic. In: Proc. Computability in Europe (CiE). LNCS, vol. 14773, pp. 218\u2013232. Springer Nature Switzerland (2024).","DOI":"10.1007\/978-3-031-64309-5_18"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Starchak, M.R.: Quantifier elimination for regular integer linear-exponential programming. In: Proceedings of the LICS (2025). to appear","DOI":"10.1109\/LICS65433.2025.00011"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Villemaire, R.: Joining $$k$$- and $$l$$-recognizable sets of natural numbers. In: Proceedings of the STACS, pp. 83\u201394. Springer Berlin Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55210-3_175","DOI":"10.1007\/3-540-55210-3_175"},{"key":"1_CR37","doi-asserted-by":"publisher","unstructured":"Villemaire, R.: The theory of $$\\langle {N}, +, {V}_k, {V}_l\\rangle $$ is undecidable. Theor. Comput. Sci. 106(2), 337\u2013349 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90256-F","DOI":"10.1016\/0304-3975(92)90256-F"},{"key":"1_CR38","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-023-00446-4","author":"H Wu","year":"2023","unstructured":"Wu, H., Chen, Y.F., Wu, Z., Xia, B., Zhan, N.: A decision procedure for string constraints with string\/integer conversion and flat regular constraints. Acta Inform. (2023). https:\/\/doi.org\/10.1007\/s00236-023-00446-4","journal-title":"Acta Inform."}],"container-title":["Lecture Notes in Computer Science","Developments in Language Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-01475-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,27]],"date-time":"2026-07-27T19:28:05Z","timestamp":1785180485000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-01475-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,17]]},"ISBN":["9783032014740","9783032014757"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-01475-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,17]]},"assertion":[{"value":"17 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"DLT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Developments in Language Theory","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Seoul","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Korea (Republic of)","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 August 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 August 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"dlt2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cida.uos.ac.kr\/dlt2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}