{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T04:12:22Z","timestamp":1750824742483,"version":"3.41.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T00:00:00Z","timestamp":1502150400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004543","name":"China Scholarship Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004543","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/I011005\/1","EP\/I010335\/1"],"award-info":[{"award-number":["EP\/I011005\/1","EP\/I010335\/1"]}],"id":[{"id":"10.13039\/501100000266","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":[[2019,1]]},"DOI":"10.1007\/s10817-017-9424-6","type":"journal-article","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T15:45:48Z","timestamp":1502207148000},"page":"69-91","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle\/HOL"],"prefix":"10.1007","volume":"62","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9886-9542","authenticated-orcid":false,"given":"Wenda","family":"Li","sequence":"first","affiliation":[]},{"given":"Grant Olney","family":"Passmore","sequence":"additional","affiliation":[]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,8]]},"reference":[{"issue":"3","key":"9424_CR1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175\u2013205 (2010)","journal-title":"J. Autom. Reason."},{"key":"9424_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics)","author":"S Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics). Springer, New York (2006)"},{"issue":"4","key":"9424_CR3","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"CW Brown","year":"2003","unstructured":"Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull. 37(4), 97\u2013108 (2003)","journal-title":"ACM SIGSAM Bull."},{"key":"9424_CR4","unstructured":"Chaieb, A., et\u00a0al.: Automated methods for formal proofs in simple arithmetics and algebra. Dissertation, Technische Universit\u00e4t, M\u00fcnchen (2008)"},{"key":"9424_CR5","doi-asserted-by":"crossref","unstructured":"Cheng, J.S., Gao, X.S., Yap, C.K.: Complete numerical isolation of real zeros in zero-dimensional triangular systems. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, pp. 92\u201399. ACM (2007)","DOI":"10.1145\/1277548.1277562"},{"key":"9424_CR6","unstructured":"Cohen, C.: Formalized algebraic numbers: construction and first-order theory. Ph.D. thesis, \u00c9cole polytechnique (2012)"},{"issue":"1: 02","key":"9424_CR7","first-page":"1","volume":"8","author":"C Cohen","year":"2012","unstructured":"Cohen, C., Mahboubi, A., et al.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci. 8(1: 02), 1\u201340 (2012)","journal-title":"Log. Methods Comput. Sci."},{"issue":"1","key":"9424_CR8","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1145\/1093390.1093393","volume":"10","author":"GE Collins","year":"1976","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition: a synopsis. ACM SIGSAM Bull. 10(1), 10\u201312 (1976)","journal-title":"ACM SIGSAM Bull."},{"key":"9424_CR9","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9424_CR10","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Passmore, G.O.: Computation in real closed infinitesimal and transcendental extensions of the rationals. In: International Conference on Automated Deduction, pp. 178\u2013192. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38574-2_12"},{"key":"9424_CR11","doi-asserted-by":"crossref","unstructured":"Denman, W., Akbarpour, B., Tahar, S., Zaki, M.H., Paulson, L.C.: Formal verification of analog designs using MetiTarski. In: Formal Methods in Computer-Aided Design, 2009. FMCAD 2009, pp. 93\u2013100. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351136"},{"key":"9424_CR12","doi-asserted-by":"crossref","unstructured":"Denman, W., Mu\u00f1oz, C.: Automated real proving in PVS via MetiTarski. In: FM 2014: Formal Methods, pp. 194\u2013199. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_14"},{"key":"9424_CR13","doi-asserted-by":"crossref","unstructured":"Denman, W., Zaki, M.H., Tahar, S., Rodrigues, L.: Towards flight control verification using automated theorem proving. In: NASA Formal Methods, pp. 89\u2013100. Springer (2011)","DOI":"10.1007\/978-3-642-20398-5_8"},{"key":"9424_CR14","doi-asserted-by":"publisher","unstructured":"Eberl, M.: A decision procedure for univariate real polynomials in Isabelle\/HOL. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP \u201915, pp. 75\u201383. ACM, New York (2015). doi: 10.1145\/2676724.2693166","DOI":"10.1145\/2676724.2693166"},{"key":"9424_CR15","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O\u2019Connor, R., Ould Biha, S., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. In: Blazy S., Paulin-Mohring C., Pichardie D. (eds.) Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22\u201326. Lecture Notes in Computer Science, vol. 7998, pp. 163\u2013179. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"9424_CR16","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: International Symposium on Functional and Logic Programming, pp. 103\u2013117. Springer (2010)","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"9424_CR17","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: K.\u00a0Schneider, J.\u00a0Brandt (eds.) Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007, Lecture Notes in Computer Science, vol. 4732, pp. 102\u2013118. Springer, Kaiserslautern (2007)","DOI":"10.1007\/978-3-540-74591-4_9"},{"key":"9424_CR18","unstructured":"H\u00f6lzl, J.: Proving inequalities over reals with computation in Isabelle\/HOL. In: International Workshop on Programming Languages for Mechanized Mathematics Systems, pp. 38\u201345 (2009)"},{"key":"9424_CR19","unstructured":"Hurd, J.: Metis first order prover. http:\/\/gilith.com\/software\/metis (2007)"},{"key":"9424_CR20","doi-asserted-by":"crossref","unstructured":"Li, W., Paulson, L.C.: A formal proof of Cauchy\u2019s residue theorem. In: ITP 2016: Seventh International Conference on Interactive Theorem Proving (2016, to appear)","DOI":"10.1007\/978-3-319-43144-4_15"},{"key":"9424_CR21","doi-asserted-by":"crossref","unstructured":"Li, W., Paulson, L.C.: A modular, efficient formalisation of real algebraic numbers. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 66\u201375. ACM (2016)","DOI":"10.1145\/2854065.2854074"},{"issue":"1","key":"9424_CR22","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1017\/S096012950600586X","volume":"17","author":"A Mahboubi","year":"2007","unstructured":"Mahboubi, A.: Implementing the cylindrical algebraic decomposition within the Coq system. Math. Struct. Comput. Sci. 17(1), 99\u2013127 (2007)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9424_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4344-1","volume-title":"Algorithmic Algebra","author":"B Mishra","year":"1993","unstructured":"Mishra, B.: Algorithmic Algebra. Springer, New York (1993)"},{"issue":"2","key":"9424_CR24","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10817-012-9256-3","volume":"51","author":"C Mu\u00f1oz","year":"2013","unstructured":"Mu\u00f1oz, C., Narkawicz, A.: Formalization of Bernstein polynomials and applications to global optimization. J. Autom. Reason. 51(2), 151\u2013196 (2013). doi: 10.1007\/s10817-012-9256-3","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9424_CR25","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/s10817-015-9320-x","volume":"54","author":"A Narkawicz","year":"2015","unstructured":"Narkawicz, A., Munoz, C., 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":"9424_CR26","unstructured":"Narkawicz, A.J., Mu\u00f1oz, C.A.: A formally-verified decision procedure for univariate polynomial computation based on Sturm\u2019s theorem. Technical Memorandum NASA\/TM-2014-218548, NASA, Langley Research Center, Hampton VA 23681-2199, USA (2014)"},{"key":"9424_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002)"},{"key":"9424_CR28","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: International Conference on Automated Deduction, pp. 748\u2013752. Springer (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"9424_CR29","doi-asserted-by":"crossref","unstructured":"Passmore, G.O., Paulson, L.C., De\u00a0Moura, L.: Real algebraic strategies for MetiTarski proofs. In: International Conference on Intelligent Computer Mathematics, pp. 358\u2013370. Springer (2012)","DOI":"10.1007\/978-3-642-31374-5_24"},{"key":"9424_CR30","unstructured":"Paulson, L.C.: Real-valued special functions: upper and lower bounds. Archive of Formal Proofs (2014)"},{"key":"9424_CR31","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: IWIL-2010, vol. 1 (2010)","DOI":"10.29007\/36dt"},{"key":"9424_CR32","unstructured":"Rahman, Q., Schmeisser, G.: Analytic Theory of Polynomials. London Mathematical Society Monographs. Clarendon Press, Oxford (2002). https:\/\/books.google.co.uk\/books?id=FzFEEVO3PXYC"},{"issue":"4","key":"9424_CR33","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s11786-011-0071-8","volume":"4","author":"M Sagraloff","year":"2010","unstructured":"Sagraloff, M.: A general approach to isolating roots of a bitstream polynomial. Math. Comput. Sci. 4(4), 481\u2013506 (2010)","journal-title":"Math. Comput. Sci."},{"key":"9424_CR34","doi-asserted-by":"crossref","unstructured":"Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with Taylor interval approximations. In: NASA Formal Methods, pp. 383\u2013397. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38088-4_26"},{"issue":"9","key":"9424_CR35","doi-asserted-by":"publisher","first-page":"1021","DOI":"10.1016\/j.jsc.2006.06.004","volume":"41","author":"AW Strzebo\u0144ski","year":"2006","unstructured":"Strzebo\u0144ski, A.W.: Cylindrical algebraic decomposition using validated numerics. J. Symb. Comput. 41(9), 1021\u20131038 (2006)","journal-title":"J. Symb. Comput."},{"key":"9424_CR36","unstructured":"Thiemann, R., Yamada, A.: Algebraic numbers in Isabelle\/HOL. Archive of Formal Proofs (2015). http:\/\/isa-afp.org\/entries\/Algebraic_Numbers.shtml . Formal proof development"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9424-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9424-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9424-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T21:07:53Z","timestamp":1750799273000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9424-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,8]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,1]]}},"alternative-id":["9424"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9424-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2017,8,8]]},"assertion":[{"value":"25 October 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 July 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 August 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}