{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T23:48:31Z","timestamp":1777765711479,"version":"3.51.4"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031974380","type":"print"},{"value":"9783031974397","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"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-031-97439-7_5","type":"book-chapter","created":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T11:03:54Z","timestamp":1756551834000},"page":"118-138","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Algorithmic Applications of\u00a0Schanuel\u2019s Conjecture"],"prefix":"10.1007","author":[{"given":"Toghrul","family":"Karimov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joris","family":"Nieuwveld","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mihir","family":"Vahanwala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Worrell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,30]]},"reference":[{"key":"5_CR1","unstructured":"Almagor, S., Chistikov, D., Ouaknine, J., Worrell, J.: O-minimal invariants for linear loops. In: 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Schloss-Dagstuhl-Leibniz Zentrum f\u00fcr Informatik (2018)"},{"issue":"2","key":"5_CR2","doi-asserted-by":"publisher","first-page":"252","DOI":"10.2307\/1970774","volume":"93","author":"J Ax","year":"1971","unstructured":"Ax, J.: On Schanuel\u2019s conjectures. Ann. Math. 93(2), 252\u2013268 (1971)","journal-title":"Ann. Math."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Baker, A.: Transcendental Number Theory. Cambridge Mathematical Library. Cambridge University Press (1975)","DOI":"10.1017\/CBO9780511565977"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Berth\u00e9, V., Karimov, T., Nieuwveld, J., Ouaknine, J., Vahanwala, M., Worrell, J.: On the decidability of monadic second-order logic with arithmetic predicates. In: Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 1\u201314 (2024)","DOI":"10.1145\/3661814.3662119"},{"key":"5_CR5","unstructured":"Bilu, Y., Luca, F., Nieuwveld, J., Ouaknine, J., Purser, D., Worrell, J.: Skolem meets schanuel. In: 47th International Symposium on Mathematical Foundations of Computer Science (2022)"},{"key":"5_CR6","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2024.103487","volume":"175","author":"E Blanchard","year":"2024","unstructured":"Blanchard, E., Hieronymi, P.: Decidability bounds for Presburger arithmetic extended by sine. Ann. Pure Appl. Logic 175, 103487 (2024)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"2","key":"5_CR7","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/321574.321591","volume":"17","author":"BF Caviness","year":"1970","unstructured":"Caviness, B.F.: On canonical forms and simplification. J. ACM 17(2), 385\u2013396 (1970)","journal-title":"J. ACM"},{"key":"5_CR8","unstructured":"Chistikov, D., Kiefer, S., Murawski, A.S., Purser, D.: The big-O problem for labelled Markov chains and weighted automata. Leibniz Int. Proc. Inform. (LIPIcs) 171, 41 (2020)"},{"key":"5_CR9","unstructured":"Chonev, V., Ouaknine, J., Worrell, J.: On the Skolem problem for continuous linear dynamical systems. In: 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Schloss-Dagstuhl-Leibniz Zentrum f\u00fcr Informatik (2016)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Chonev, V., Ouaknine, J., Worrell, J.: On the zeros of exponential polynomials. J. ACM 70(4), 26:1\u201326:26 (2023)","DOI":"10.1145\/3603543"},{"key":"5_CR11","unstructured":"Daviaud, L., Jurdzi\u0144ski, M., Lazi\u0107, R., Mazowiecki, F., P\u00e9rez, G.A., Worrell, J.: When is containment decidable for probabilistic automata? In: 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, p. 121. Schloss Dagstuhl-Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing (2018)"},{"issue":"2","key":"5_CR12","doi-asserted-by":"publisher","first-page":"169","DOI":"10.2307\/2269808","volume":"31","author":"CC Elgot","year":"1966","unstructured":"Elgot, C.C., Rabin, M.O.: Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. J. Symb. Logic 31(2), 169\u2013181 (1966)","journal-title":"J. Symb. Logic"},{"issue":"225","key":"5_CR13","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1090\/S0025-5718-99-00995-3","volume":"68","author":"HRP Ferguson","year":"1999","unstructured":"Ferguson, H.R.P., Bailey, D.H., Arno, S.: Analysis of PSLQ, an integer relation finding algorithm. Math. Comput. 68(225), 351\u2013369 (1999)","journal-title":"Math. Comput."},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-14162-1_44","volume-title":"Automata, Languages and Programming","author":"H Gimbert","year":"2010","unstructured":"Gimbert, H., Oualhadj, Y.: Probabilistic automata on finite words: decidable and undecidable problems. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 527\u2013538. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14162-1_44"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Gonek, S.M., Montgomery, H.L.: Kronecker\u2019s approximation theorem. Indagationes Mathematicae 27(2), 506\u2013523 (2016). In Memoriam J.G. Van der Corput (1890\u20131975) Part 2","DOI":"10.1016\/j.indag.2016.02.002"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-030-99527-0_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Zingg","year":"2022","unstructured":"Zingg, S., Krsti\u0107, S., Raszyk, M., Schneider, J., Traytel, D.: Verified first-order monitoring with recursive rules. In: TACAS 2022. LNCS, vol. 13244, pp. 236\u2013253. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_13"},{"key":"5_CR17","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1016\/j.jsc.2017.07.007","volume":"85","author":"C-C Huang","year":"2018","unstructured":"Huang, C.-C., Li, J.-C., Ming, X., Li, Z.-B.: Positive root isolation for poly-powers by exclusion and differentiation. J. Symb. Comput. 85, 148\u2013169 (2018)","journal-title":"J. Symb. Comput."},{"key":"5_CR18","unstructured":"Kenison, G.: The threshold problem for hypergeometric sequences with quadratic parameters. In: 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2024)"},{"key":"5_CR19","unstructured":"Lang, S.: Introduction to Transcendental Numbers. Addison-Wesley series in mathematics. Addison-Wesley Publishing Company (1966)"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Lang, S.: Algebra. Graduate Texts in Mathematics, 3rd edn. Springer, New York (2002)","DOI":"10.1007\/978-1-4613-0041-0_1"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Macintyre, A.: Turing meets Schanuel. Ann. Pure Appl. Logic 167(10), 901\u2013938 (2016). Logic Colloquium 2012","DOI":"10.1016\/j.apal.2015.10.003"},{"key":"5_CR22","first-page":"451","volume":"115","author":"A Macintyre","year":"1996","unstructured":"Macintyre, A., Wilkie, A., Odifreddi, P.: On the decidability of the real exponential field. Kreisel\u2019s Math. 115, 451 (1996)","journal-title":"Kreisel\u2019s Math."},{"key":"5_CR23","unstructured":"Majumdar, R., Salamati, M., Soudjani, S.: On decidability of time-bounded reachability in CTMDPs. In: 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Schloss-Dagstuhl-Leibniz Zentrum f\u00fcr Informatik (2020)"},{"key":"5_CR24","unstructured":"Mariaule, N.: On the decidability of the p-adic exponential ring. The University of Manchester (United Kingdom) (2013)"},{"issue":"1","key":"5_CR25","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. Theoret. Comput. Sci. 304(1), 1\u201333 (2003)","journal-title":"Theoret. Comput. Sci."},{"key":"5_CR26","unstructured":"Paz, A.: Introduction to probabilistic automata (Computer science and applied mathematics). Academic Press, Inc., USA (1971)"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Richardson, D.: A simplified method of recognizing zero among elementary constants. In: Proceedings of the 1995 International Symposium on Symbolic and Algebraic Computation, pp. 104\u2013109 (1995)","DOI":"10.1145\/220346.220360"},{"issue":"6","key":"5_CR28","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1006\/jsco.1997.0157","volume":"24","author":"D Richardson","year":"1997","unstructured":"Richardson, D.: How to Recognize Zero. J. Symb. Comput. 24(6), 627\u2013645 (1997)","journal-title":"J. Symb. Comput."},{"key":"5_CR29","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s11786-007-0002-x","volume":"1","author":"D Richardson","year":"2007","unstructured":"Richardson, D.: Zero tests for constants in simple scientific computation. Math. Comput. Sci. 1, 21\u201337 (2007)","journal-title":"Math. Comput. Sci."},{"key":"5_CR30","doi-asserted-by":"publisher","first-page":"485","DOI":"10.2140\/pjm.1976.65.485","volume":"65","author":"M Rosenlicht","year":"1976","unstructured":"Rosenlicht, M.: On Liouville\u2019s theory of elementary functions. Pac. J. Math. 65, 485\u2013492 (1976)","journal-title":"Pac. J. Math."},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition, Vienna, pp. 24\u201384. Springer Vienna (1998)","DOI":"10.1007\/978-3-7091-9459-1_3"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Alfred Tarski. A Decision Method for Elementary Algebra and Geometry. In Bob\u00a0F. Caviness and Jeremy\u00a0R. Johnson, editors, Quantifier Elimination and Cylindrical Algebraic Decomposition, pages 24\u201384, Vienna, 1998. Springer Vienna","DOI":"10.1007\/978-3-7091-9459-1_3"},{"key":"5_CR33","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2024.106481","volume":"186","author":"M Vahanwala","year":"2024","unstructured":"Vahanwala, M.: Skolem and positivity completeness of ergodic Markov chains. Inf. Process. Lett. 186, 106481 (2024)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"5_CR34","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1016\/0304-3975(91)90381-B","volume":"88","author":"A Weber","year":"1991","unstructured":"Weber, A., Seidl, H.: On the degree of ambiguity of finite automata. Theoret. Comput. Sci. 88(2), 325\u2013349 (1991)","journal-title":"Theoret. Comput. Sci."},{"issue":"4","key":"5_CR35","doi-asserted-by":"publisher","first-page":"1051","DOI":"10.1090\/S0894-0347-96-00216-0","volume":"9","author":"AJ Wilkie","year":"1996","unstructured":"Wilkie, A.J.: Model completeness results for expansions of the ordered field of real numbers by restricted pfaffian functions and the exponential function. J. Am. Math. Soc. 9(4), 1051\u20131094 (1996)","journal-title":"J. Am. Math. Soc."},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Wilkie, A.J.: Schanuel\u2019s Conjecture and the Decidability of the Real Exponential Field, pp. 223\u2013230. Springer, Dordrecht (1997)","DOI":"10.1007\/978-94-015-8923-9_11"},{"key":"5_CR37","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104634","volume":"275","author":"X Ming","year":"2020","unstructured":"Ming, X., Deng, Y.: Time-bounded termination analysis for probabilistic programs with delays. Inf. Comput. 275, 104634 (2020)","journal-title":"Inf. Comput."},{"issue":"1","key":"5_CR38","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.apal.2004.07.001","volume":"132","author":"B Zilber","year":"2005","unstructured":"Zilber, B.: Pseudo-exponentiation on algebraically closed fields of characteristic zero. Ann. Pure Appl. Logic 132(1), 67\u201395 (2005)","journal-title":"Ann. Pure Appl. Logic"}],"container-title":["Lecture Notes in Computer Science","Principles of Formal Quantitative Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-97439-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T15:28:34Z","timestamp":1777476514000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-97439-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,30]]},"ISBN":["9783031974380","9783031974397"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-97439-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,30]]},"assertion":[{"value":"30 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}