{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T08:13:42Z","timestamp":1742804022639,"version":"3.37.3"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,4,3]],"date-time":"2019-04-03T00:00:00Z","timestamp":1554249600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["742178"],"award-info":[{"award-number":["742178"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,2]]},"DOI":"10.1007\/s10817-019-09521-3","type":"journal-article","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T01:58:37Z","timestamp":1554343117000},"page":"331-360","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle\/HOL"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9886-9542","authenticated-orcid":false,"given":"Wenda","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0288-4279","authenticated-orcid":false,"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,3]]},"reference":[{"key":"9521_CR1","volume-title":"Ordinary Differential Equations","author":"VI Arnold","year":"1992","unstructured":"Arnold, V.I.: Ordinary Differential Equations. Springer, Berlin (1992)"},{"key":"9521_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry","author":"S Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry. Springer, Berlin (2006)"},{"key":"9521_CR3","unstructured":"Brunel, A.: Non-constructive complex analysis in Coq. In: Danielsson, N.A., Nordstr\u00f6m, B. (eds.) 18th International Workshop on Types for Proofs and Programs (TYPES 2011), pp. 1\u201315. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2013)"},{"key":"9521_CR4","doi-asserted-by":"crossref","unstructured":"Collins, G.E., Krandick, W.: An efficient algorithm for infallible polynomial complex root isolation. In: Proceedings of International Symposium on Symbolic and Algebraic Computation, ISSAC \u201992, pp. 189\u2013194. ACM (1992)","DOI":"10.1145\/143242.143308"},{"key":"9521_CR5","doi-asserted-by":"crossref","unstructured":"Eberl, M.: A decision procedure for univariate real polynomials in Isabelle\/HOL. In: Conference on Certified Programs and Proofs, pp. 75\u201383. ACM Press (2015)","DOI":"10.1145\/2676724.2693166"},{"issue":"9","key":"9521_CR6","doi-asserted-by":"publisher","first-page":"715","DOI":"10.4169\/amer.math.monthly.119.09.715","volume":"119","author":"M Eisermann","year":"2012","unstructured":"Eisermann, M.: The fundamental theorem of algebra made effective: an elementary real-algebraic proof via Sturm chains. Am. Math. Mon. 119(9), 715 (2012)","journal-title":"Am. Math. Mon."},{"key":"9521_CR7","unstructured":"Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, vol. 10, no. 23, pp. 151\u2013165. University of Bia\u0142ystok (2007). \nhttp:\/\/mizar.org\/trybulec65\/\n\n. Accessed 2 Apr 2019"},{"key":"9521_CR8","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s10817-009-9145-6","volume":"43","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Formalizing an analytic proof of the prime number theorem (Dedicated to Mike Gordon on the occasion of his 60th birthday). J. Autom. Reason. 43, 243\u2013261 (2009)","journal-title":"J. Autom. Reason."},{"key":"9521_CR9","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-39634-2_21","volume-title":"Interactive Theorem Proving","author":"Johannes H\u00f6lzl","year":"2013","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: Volume\u00a07998, pp. 279\u2013294 (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39634-2_21"},{"key":"9521_CR10","unstructured":"Li, W.: The Sturm\u2013Tarski theorem. In: Archive of Formal Proofs (2014). \nhttp:\/\/isa-afp.org\/entries\/Sturm_Tarski.html\n\n. Accessed 2 Apr 2019"},{"key":"9521_CR11","unstructured":"Li, W.: Count the number of complex roots. In: Archive of Formal Proofs (2017). \nhttp:\/\/isa-afp.org\/entries\/Count_Complex_Roots.html\n\n. Accessed 2 Apr 2019"},{"key":"9521_CR12","unstructured":"Li, W.: Evaluate winding numbers through cauchy indices. In: Archive of Formal Proofs (2017). \nhttp:\/\/isa-afp.org\/entries\/Winding_Number_Eval.html\n\n. Accessed 2 Apr 2019"},{"key":"9521_CR13","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10817-017-9424-6","volume":"62","author":"W Li","year":"2017","unstructured":"Li, W., Passmore, G.O., Paulson, L.C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle\/HOL. J Autom Reason 62, 69\u201391 (2017). \nhttps:\/\/doi.org\/10.1007\/s10817-017-9424-6","journal-title":"J Autom Reason"},{"key":"9521_CR14","doi-asserted-by":"crossref","unstructured":"Li, W., Paulson, L.C.: A formal proof of Cauchy\u2019s residue theorem. In: Blanchette, J.C., Merz, S., (eds.) 7th International Conference on Interactive Theorem Proving, pp. 235\u2013251. Springer (2016)","DOI":"10.1007\/978-3-319-43144-4_15"},{"issue":"1","key":"9521_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-8(1:2)2012","volume":"8","author":"A Mahboubi","year":"2012","unstructured":"Mahboubi, A., Cohen, C.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci. 8(1), 1\u201340 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"9521_CR16","doi-asserted-by":"publisher","DOI":"10.1090\/surv\/003","volume-title":"Geometry of Polynomials","author":"M Marden","year":"1949","unstructured":"Marden, M.: Geometry of Polynomials, 2nd edn. American Mathematical Society, Providence (1949)","edition":"2"},{"key":"9521_CR17","volume-title":"Automated Deduction \u2013 CADE-20. CADE 2005. Lecture Notes in Computer Science","author":"S McLaughlin","year":"2005","unstructured":"McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20. CADE 2005. Lecture Notes in Computer Science, vol. 3632. Springer, Berlin (2005)"},{"issue":"4","key":"9521_CR18","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/s10817-015-9320-x","volume":"54","author":"A Narkawicz","year":"2015","unstructured":"Narkawicz, A., Mu\u00f1oz, C.A., Dutle, A.: Formally-verified decision procedures for univariate polynomial computation based on Sturm\u2019s and Tarski\u2019s theorems. J. Autom. Reason. 54(4), 285\u2013326 (2015)","journal-title":"J. Autom. Reason."},{"key":"9521_CR19","volume-title":"Analytic Theory of Polynomials (2002)","author":"QI Rahman","year":"2016","unstructured":"Rahman, Q.I., Schmeisser, G.: Analytic Theory of Polynomials (2002). Oxford University Press, Oxford (2016)"},{"issue":"3","key":"9521_CR20","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1145\/322077.322084","volume":"25","author":"HS Wilf","year":"1978","unstructured":"Wilf, H.S.: A global bisection algorithm for computing the zeros of polynomials in the complex plane. J. ACM 25(3), 415\u2013420 (1978)","journal-title":"J. ACM"},{"key":"9521_CR21","doi-asserted-by":"crossref","unstructured":"Yap, C.K., Sagraloff, M.: A simple but exact and efficient algorithm for complex root isolation. In: 36th International Symposium on Symbolic and Algebraic Computation, ISSAC \u201911, pp. 353\u2013360. ACM Press (2011)","DOI":"10.1145\/1993886.1993938"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09521-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-019-09521-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09521-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,2]],"date-time":"2020-04-02T11:45:09Z","timestamp":1585827909000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-019-09521-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,3]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,2]]}},"alternative-id":["9521"],"URL":"https:\/\/doi.org\/10.1007\/s10817-019-09521-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2019,4,3]]},"assertion":[{"value":"25 July 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 March 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 April 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}