{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:52:11Z","timestamp":1781927531177,"version":"3.54.5"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,1,25]],"date-time":"2025-01-25T00:00:00Z","timestamp":1737763200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,25]],"date-time":"2025-01-25T00:00:00Z","timestamp":1737763200000},"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":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,3]]},"DOI":"10.1007\/s10817-024-09716-3","type":"journal-article","created":{"date-parts":[[2025,1,25]],"date-time":"2025-01-25T08:30:47Z","timestamp":1737793847000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem"],"prefix":"10.1007","volume":"69","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-0428-4403","authenticated-orcid":false,"given":"Enrico","family":"Lipparini","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1710-1513","authenticated-orcid":false,"given":"Stefan","family":"Ratschan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,1,25]]},"reference":[{"issue":"205","key":"9716_CR1","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1090\/S0025-5718-1994-1203731-4","volume":"62","author":"O Aberth","year":"1994","unstructured":"Aberth, O.: Computation of topological degree using interval arithmetic, and applications. Math. Comput. 62(205), 171\u2013178 (1994)","journal-title":"Math. Comput."},{"key":"9716_CR2","unstructured":"Ait-Aoudia, S., J\u00e9gou, R., Michelucci, D.: Reduction of constraint systems. CoRR (2014). Arxiv:abs\/1405.6131"},{"key":"9716_CR3","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Johnson, T.T.: Hyst: A source transformation and translation tool for hybrid automaton models. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC \u201915, pp. 128\u2013133. Association for Computing Machinery, New York (2015)","DOI":"10.1145\/2728606.2728630"},{"issue":"10","key":"9716_CR4","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1145\/3587692","volume":"66","author":"H Barbosa","year":"2023","unstructured":"Barbosa, H., Barrett, C., Cook, B., Dutertre, B., Kremer, G., Lachnitt, H., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Tinelli, C., Zohar, Y.: Generating and exploiting automated reasoning proof certificates. Commun. ACM 66(10), 86\u201395 (2023)","journal-title":"Commun. ACM"},{"key":"9716_CR5","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Reynolds, A., Kremer, G., Lachnitt, H., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Viswanathan, A., Viteri, S., Zohar, Y., Tinelli, C., Barrett, C.: Flexible proof production in an industrial-strength SMT solver. In: Automated Reasoning: 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8\u201310, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pp. 15\u201335. Springer, Berlin (2022)","DOI":"10.1007\/978-3-031-10769-6_3"},{"key":"9716_CR6","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M. J. H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185, chap 26, pp. 825\u2013885. IOS Press (2009). http:\/\/theory.stanford.edu\/~barrett\/pubs\/BSST09.pdf"},{"key":"9716_CR7","doi-asserted-by":"crossref","unstructured":"Brau\u00dfe, F., Korovin, K., Korovina, M., M\u00fcller, N.: The ksmt Calculus Is a $$\\delta $$-Complete Decision Procedure for Non-linear Constraints, volume 12699 of Lecture Notes in Computer Science, pp. 113\u2013130. Springer (2021)","DOI":"10.1007\/978-3-030-79876-5_7"},{"key":"9716_CR8","doi-asserted-by":"crossref","DOI":"10.1016\/j.jsc.2023.102250","volume":"121","author":"R Chen","year":"2024","unstructured":"Chen, R., Li, H., Xia, B., Zhao, T., Zheng, T.: Isolating all the real roots of a mixed trigonometric-polynomial. J. Symb. Comput. 121, 102250 (2024)","journal-title":"J. Symb. Comput."},{"key":"9716_CR9","doi-asserted-by":"crossref","unstructured":"Chen, R., Xia, B.: Deciding first-order formulas involving univariate mixed trigonometric-polynomials. In: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation (2023)","DOI":"10.1145\/3597066.3597104"},{"key":"9716_CR10","doi-asserted-by":"crossref","unstructured":"Chen, R., Xia, B.: Reduction of transcendental decision problems over the reals. In: Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201924, pp. 56\u201364. Association for Computing Machinery, New York (2024)","DOI":"10.1145\/3666000.3669675"},{"issue":"3","key":"9716_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3230639","volume":"19","author":"A Cimatti","year":"2018","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Logic 19(3), 1\u201352 (2018)","journal-title":"ACM Trans. Comput. Logic"},{"key":"9716_CR12","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N. Smolka, S. (eds.) Proceedings of TACAS, vol. 7795 of LNCS. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"9716_CR13","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201908\/ETAPS\u201908, pp. 337\u2013340. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9716_CR14","doi-asserted-by":"crossref","unstructured":"Dinca, G., Mawhin, J.: Brouwer Degree: The Core of Nonlinear Analysis. Birkh\u00e4user (2021)","DOI":"10.1007\/978-3-030-63230-4"},{"key":"9716_CR15","doi-asserted-by":"crossref","first-page":"517","DOI":"10.4153\/CJM-1958-052-0","volume":"10","author":"AL Dulmage","year":"1958","unstructured":"Dulmage, A.L., Mendelsohn, N.S.: Coverings of bipartite graphs. Can. J. Math. 10, 517\u2013534 (1958)","journal-title":"Can. J. Math."},{"key":"9716_CR16","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198511960.001.0001","volume-title":"Degree Theory in Analysis and Applications","author":"I Fonseca","year":"1995","unstructured":"Fonseca, I., Gangbo, W.: Degree Theory in Analysis and Applications. Clarendon Press, Oxford (1995)"},{"issue":"3","key":"9716_CR17","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/s41468-017-0009-6","volume":"1","author":"P Franek","year":"2018","unstructured":"Franek, P., Kr\u010d\u00e1l, M., Wagner, H.: Solving equations and optimization problems with uncertainty. J. Appl. Comput. Topol. 1(3), 297\u2013330 (2018)","journal-title":"J. Appl. Comput. Topol."},{"key":"9716_CR18","doi-asserted-by":"crossref","first-page":"1265","DOI":"10.1090\/S0025-5718-2014-02877-9","volume":"84","author":"P Franek","year":"2015","unstructured":"Franek, P., Ratschan, S.: Effective topological degree computation based on interval arithmetic. Math. Comput. 84, 1265\u20131290 (2015)","journal-title":"Math. Comput."},{"issue":"2","key":"9716_CR19","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/s10817-015-9351-3","volume":"57","author":"P Franek","year":"2016","unstructured":"Franek, P., Ratschan, S., Zgliczynski, P.: Quasi-decidability of a fragment of the first-order theory of real numbers. J. Autom. Reason. 57(2), 157\u2013185 (2016)","journal-title":"J. Autom. Reason."},{"key":"9716_CR20","first-page":"209","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. JSAT 1, 209\u2013236 (2007)","journal-title":"JSAT"},{"key":"9716_CR21","doi-asserted-by":"crossref","unstructured":"Fu, Z., Su, Z.: Xsat: A fast floating-point satisfiability solver. In: CAV, volume 9780 of Lecture Notes in Computer Science, pp. 187\u2013209. Springer (2016)","DOI":"10.1007\/978-3-319-41540-6_11"},{"key":"9716_CR22","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: An SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (eds.) Automated Deduction\u2014CADE-24, pp. 208\u2013214. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38574-2_14"},{"issue":"1","key":"9716_CR23","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1112\/jlms\/s1-10.37.26","volume":"s1\u201310","author":"P Hall","year":"1935","unstructured":"Hall, P.: On representatives of subsets. J. Lond. Math. Soc. s1\u201310(1), 26\u201330 (1935)","journal-title":"J. Lond. Math. Soc."},{"key":"9716_CR24","volume-title":"Global Optimization Using Interval Analysis","author":"E Hansen","year":"1992","unstructured":"Hansen, E.: Global Optimization Using Interval Analysis. Marcel Dekker, New York (1992)"},{"key":"9716_CR25","doi-asserted-by":"crossref","unstructured":"Huang, C.-C., Li, J.-C., Xu, M., Li, Z.-B.: Positive root isolation for poly-powers by exclusion and differentiation. J. Symb. Comput. 85, 148\u2013169 (2018). (41th International Symposium on Symbolic and Alge-braic Computation (ISSAC\u201916))","DOI":"10.1016\/j.jsc.2017.07.007"},{"issue":"1","key":"9716_CR26","first-page":"89","volume":"83","author":"RB Kearfott","year":"1998","unstructured":"Kearfott, R.B.: On proving existence of feasible points in equality constrained optimization problems. Math. Program. 83(1), 89\u2013100 (1998)","journal-title":"Math. Program."},{"key":"9716_CR27","doi-asserted-by":"crossref","unstructured":"Kremer, G., Reynolds, A., Barrett, C., Tinelli, C.: Cooperating techniques for solving nonlinear real arithmetic in the cvc5 SMT solver (system description). In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning, pp. 95\u2013105. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-10769-6_7"},{"key":"9716_CR28","volume-title":"Introduction to Smooth Manifolds","author":"JM Lee","year":"2000","unstructured":"Lee, J.M.: Introduction to Smooth Manifolds. Springer, New York (2000)"},{"key":"9716_CR29","doi-asserted-by":"crossref","unstructured":"Lipparini, E., Cimatti, A., Griggio, A., Sebastiani, R.: Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test. In: Bouajjani, A., Hol\u00edk, L., Wu, Z. (eds.) Automated Technology for Verification and Analysis, pp. 137\u2013153. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-19992-9_9"},{"key":"9716_CR30","doi-asserted-by":"crossref","unstructured":"Lipparini, E., Ratschan, S.: Satisfiability of non-linear transcendental arithmetic as a certificate search problem. In: Proceedings of the NASA Formal Methods Symposium, LNCS. Springer (2023)","DOI":"10.1007\/978-3-031-33170-1_29"},{"key":"9716_CR31","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/0377-0427(94)00089-J","volume":"60","author":"G Mayer","year":"1994","unstructured":"Mayer, G.: Epsilon-inflation in verification algorithms. J. Comput. Appl. Math. 60, 147\u2013169 (1994)","journal-title":"J. Comput. Appl. Math."},{"issue":"1","key":"9716_CR32","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1016\/j.jsc.2011.08.004","volume":"47","author":"S McCallum","year":"2012","unstructured":"McCallum, S., Weispfenning, V.: Deciding polynomial-transcendental problems. J. Symb. Comput. 47(1), 16\u201331 (2012)","journal-title":"J. Symb. Comput."},{"issue":"2","key":"9716_CR33","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"RM McConnell","year":"2011","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119\u2013161 (2011)","journal-title":"Comput. Sci. Rev."},{"key":"9716_CR34","volume-title":"Topology from the Differentiable Viewpoint","author":"JW Milnor","year":"1997","unstructured":"Milnor, J.W.: Topology from the Differentiable Viewpoint. Princeton University Press, Princeton (1997)"},{"key":"9716_CR35","doi-asserted-by":"crossref","DOI":"10.1137\/1.9780898717716","volume-title":"Introduction to Interval Analysis","author":"RE Moore","year":"2009","unstructured":"Moore, R.E., Baker Kearfott, R., Cloud, M.J.: Introduction to Interval Analysis. SIAM, Philadelphia (2009)"},{"key":"9716_CR36","volume-title":"Analysis on Manifolds","author":"JR Munkres","year":"1991","unstructured":"Munkres, J.R.: Analysis on Manifolds. CRC Press, Boca Raton (1991)"},{"key":"9716_CR37","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511526473","volume-title":"Interval Methods for Systems of Equations","author":"A Neumaier","year":"1991","unstructured":"Neumaier, A.: Interval Methods for Systems of Equations. Cambridge University Press, Cambridge (1991)"},{"key":"9716_CR38","doi-asserted-by":"crossref","unstructured":"Ni, X., Wu, Y., Xia, B.: Solving smt over non-linear real arithmetic via numerical sampling and symbolic verification. In: Dependable Software Engineering. Theories, Tools, and Applications: 9th International Symposium, SETTA 2023, Nanjing, China, November 27\u201329, 2023, Proceedings, pp. 171\u2013188. Springer, Berlin (2023)","DOI":"10.1007\/978-981-99-8664-4_10"},{"key":"9716_CR39","unstructured":"O\u2019Regan, D., Cho, Y.J., Chen, Y.: Topological Degree Theory and Applications, p. 3. Taylor and Francis, Milton Park (2006)"},{"key":"9716_CR40","unstructured":"Ratschan, S.: Deciding predicate logical theories of real-valued functions. In: Leroux, J., Lombardy, S., Peleg, D. (eds.) 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023), volume 272 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 76:1\u201376:15. Dagstuhl, Germany (2023)"},{"issue":"4","key":"9716_CR41","doi-asserted-by":"crossref","first-page":"514","DOI":"10.2307\/2271358","volume":"33","author":"D Richardson","year":"1968","unstructured":"Richardson, D.: Some undecidable problems involving elementary functions of a real variable. J. Symb. Log. 33(4), 514\u2013520 (1968)","journal-title":"J. Symb. Log."},{"key":"9716_CR42","doi-asserted-by":"crossref","unstructured":"Roohi, N., Prabhakar, P., Viswanathan, M.: Hare: A hybrid abstraction refinement engine for verifying non-linear hybrid automata. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 573\u2013588. Springer, Berlin (2017)","DOI":"10.1007\/978-3-662-54577-5_33"},{"key":"9716_CR43","doi-asserted-by":"crossref","unstructured":"Rump, S.M.: Verification methods: Rigorous results using floating-point arithmetic. Acta Numer., 3\u20134 (2010)","DOI":"10.1145\/1837934.1837937"},{"key":"9716_CR44","doi-asserted-by":"crossref","unstructured":"Strzebonski, A.: Real root isolation for tame elementary functions. In: Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201909, pp. 341\u2013350. Association for Computing Machinery, New York (2009)","DOI":"10.1145\/1576702.1576749"},{"issue":"3","key":"9716_CR45","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1016\/j.jsc.2011.11.004","volume":"47","author":"A Strzeboski","year":"2012","unstructured":"Strzeboski, A.: Real root isolation for exp-log-arctan functions. J. Symb. Comput. 47(3), 282\u2013314 (2012)","journal-title":"J. Symb. Comput."},{"key":"9716_CR46","first-page":"12","volume":"51","author":"VX Tung","year":"2017","unstructured":"Tung, V.X., Khanh, T., Ogawa, M.: raSAT: an SMT solver for polynomial constraints. Form. Methods Syst. Des. 51, 12 (2017)","journal-title":"Form. Methods Syst. Des."},{"issue":"28","key":"9716_CR47","doi-asserted-by":"crossref","first-page":"5111","DOI":"10.1021\/jp970984n","volume":"101","author":"DJ Wales","year":"1997","unstructured":"Wales, D.J., Doye, J.P.K.: Global optimization by basin-hopping and the lowest energy structures of Lennard-Jones clusters containing up to 110 atoms. J. Phys. Chem. A 101(28), 5111\u20135116 (1997)","journal-title":"J. Phys. Chem. A"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09716-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09716-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09716-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T20:54:10Z","timestamp":1742676850000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09716-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,25]]},"references-count":47,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3]]}},"alternative-id":["9716"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09716-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,25]]},"assertion":[{"value":"2 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 December 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 January 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"3"}}