{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T06:15:10Z","timestamp":1777616110322,"version":"3.51.4"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,7,18]],"date-time":"2012-07-18T00:00:00Z","timestamp":1342569600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,8]]},"DOI":"10.1007\/s10817-012-9256-3","type":"journal-article","created":{"date-parts":[[2012,7,19]],"date-time":"2012-07-19T00:51:12Z","timestamp":1342659072000},"page":"151-196","source":"Crossref","is-referenced-by-count":49,"title":["Formalization of Bernstein Polynomials and Applications to Global Optimization"],"prefix":"10.1007","volume":"51","author":[{"given":"C\u00e9sar","family":"Mu\u00f1oz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anthony","family":"Narkawicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,7,18]]},"reference":[{"issue":"3","key":"9256_CR1","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175\u2013205 (2010)","journal-title":"J. Autom. Reason."},{"key":"9256_CR2","unstructured":"Alford, J.: Translation of Bernstein coefficients under an affine mapping of the unit interval. Technical Memorandum NASA\/TM-2012-217557, NASA Langley Research Center (2012)"},{"key":"9256_CR3","unstructured":"Archer, M., Di Vito, B., Mu\u00f1oz, C. (eds.): Design and Application of Strategies\/Tactics in Higher Order Logics. No. NASA\/CP-2003-212448, NASA, Langley Research Center, Hampton VA 23681-2199, USA (2003)"},{"key":"9256_CR4","unstructured":"Bertot, Y., Guilhot, F., Mahboubi, A.: A formal study of Bernstein coefficients and polynomials. Tech. Rep. INRIA-005030117, INRIA (2010)"},{"key":"9256_CR5","first-page":"85","volume-title":"Proceedings of the NASA Formal Methods Symposium (NFM 2012). Lecture Notes in Computer Science, vol. 7226","author":"N Brisebarre","year":"2012","unstructured":"Brisebarre, N., Joldes, M., Martin-Dorel, \u00c9., Mayero, M., Muller, J.M., Pasca, I., Rideau, L., Th\u00e9ry, L.: Rigorous polynomial approximation using Taylor models in Coq. In: Goodloe, A., Person, S. (eds.) Proceedings of the NASA Formal Methods Symposium (NFM 2012). Lecture Notes in Computer Science, vol. 7226, pp. 85\u201399. Springer, Norfolk, US (2012)","edition":"7226"},{"key":"9256_CR6","unstructured":"de\u00a0Casteljau, P.: Formes \u00e0 p\u00f4les. Herm\u00e8s (1985)"},{"key":"9256_CR7","unstructured":"Ch\u00e1ves, F., Daumas, M.: A library of Taylor models for PVS automatic proof checker. Technical Report RR2006-07, \u00c9cole Normale Sup\u00e9rieure de Lyon (2006)"},{"issue":"1:02","key":"9256_CR8","first-page":"1","volume":"8","author":"C Cohen","year":"2012","unstructured":"Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logical Methods in Computer Science (LMCS) 8(1:02), 1\u201340 (2012)","journal-title":"Logical Methods in Computer Science (LMCS)"},{"key":"9256_CR9","doi-asserted-by":"crossref","unstructured":"Collins, G.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Second GI Conference on Automata Theory and Formal Languages. Lecture Notes in Computer Science, vol.\u00a033, pp. 134\u2013183. Springer, Kaiserslautern (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"9256_CR10","doi-asserted-by":"crossref","unstructured":"Crespo, L.G., Mu\u00f1oz, C.A., Narkawicz, A.J., Kenny, S.P., Giesy, D.P.: Uncertainty analysis via failure domain characterization: polynomial requirement functions. In: Proceedings of European Safety and Reliability Conference. Troyes, France (2011)","DOI":"10.1201\/b11433-162"},{"issue":"2","key":"9256_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/TC.2008.213","volume":"58","author":"M Daumas","year":"2009","unstructured":"Daumas, M., Lester, D., Mu\u00f1oz, C.: Verified real number calculations: a library for interval arithmetic. IEEE Trans. Comput. 58(2), 1\u201312 (2009)","journal-title":"IEEE Trans. Comput."},{"key":"9256_CR12","unstructured":"Delahaye, D., Mayero, M.: Field, une proc\u00e9dure de d\u00e9cision pour les nombres r\u00e9els en coq. In: Cast\u00e9ran, P. (ed.) Journ\u00e9es Francophones des Langages Applicatifs (JFLA\u201901), pp. 33\u201348. Collection Didactique, INRIA, Pontarlier, France, Janvier (2001)"},{"key":"9256_CR13","unstructured":"Di Vito, B.: Manip user\u2019s guide, version 1.3. Technical Memorandum NASA\/TM-2002-211647, NASA Langley Research Center (2002)"},{"issue":"2","key":"9256_CR14","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1109\/TC.2010.128","volume":"60","author":"F Dinechin de","year":"2011","unstructured":"de\u00a0Dinechin, F., Lauter, C., Melquiond, G.: Certifying the floating-point implementation of an elementary function using Gappa. IEEE Trans. Comput. 60(2), 242\u2013253 (2011)","journal-title":"IEEE Trans. Comput."},{"key":"9256_CR15","first-page":"37","volume-title":"Proceedings of the International Symposium on interval mathematics on Interval mathematics 1985","author":"J Garloff","year":"1985","unstructured":"Garloff, J.: Convergent bounds for the range of multivariate polynomials. In: Proceedings of the International Symposium on interval mathematics on Interval mathematics 1985, pp. 37\u201356. Springer-Verlag, London, UK (1985)"},{"key":"9256_CR16","first-page":"154","volume":"4","author":"J Garloff","year":"1993","unstructured":"Garloff, J.: The Bernstein algorithm. Interval Comput. 4, 154\u2013168 (1993)","journal-title":"Interval Comput."},{"key":"9256_CR17","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1023\/A:1009934614393","volume":"6","author":"J Garloff","year":"2000","unstructured":"Garloff, J.: Application of Bernstein expansion to the solution of control problems. Reliab. Comput. 6, 303\u2013320 (2000)","journal-title":"Reliab. Comput."},{"issue":"1","key":"9256_CR18","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1145\/1132973.1132980","volume":"32","author":"L Granvilliers","year":"2006","unstructured":"Granvilliers, L., Benhamou, F.: RealPaver: an interval solver using constraint satisfaction techniques. ACM Trans. Math. Softw. 32(1), 138\u2013156 (2006)","journal-title":"ACM Trans. Math. Softw."},{"key":"9256_CR19","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: a survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995)"},{"key":"9256_CR20","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 4732, pp. 102\u2013118. Springer (2007)","DOI":"10.1007\/978-3-540-74591-4_9"},{"key":"9256_CR21","doi-asserted-by":"crossref","unstructured":"Hunt, W.A., Jr., Krug, R.B., Moore, J.S.: Linear and nonlinear arithmetic in ACL2. In: Geist, D., Tronci, E. (eds.) Proceedings of Correct Hardware Design and Verification Methods (CHARME). Lecture Notes in Computer Science, vol. 2860, pp. 319\u2013333. Springer, L\u2019Aquila, Italy (2003)","DOI":"10.1007\/978-3-540-39724-3_29"},{"key":"9256_CR22","volume-title":"Approximate Commutative Algebra. Texts and Monographs in Symbolic Computation","author":"EL Kaltofen","year":"2010","unstructured":"Kaltofen, E.L., Li, B., Yang, Z., Zhi, L.: Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients. In: Robbiano, L., Abbott, J. (eds.) Approximate Commutative Algebra. Texts and Monographs in Symbolic Computation, Springer Vienna (2010)"},{"issue":"4","key":"9256_CR23","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1109\/6979.898217","volume":"1","author":"J Kuchar","year":"2000","unstructured":"Kuchar, J., Yang, L.: A review of conflict detection and resolution modeling methods. IEEE Trans. Intell. Transp. Syst. 1(4), 179\u2013189 (2000)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"9256_CR24","volume-title":"Bernstein Polynomials","author":"GG Lorentz","year":"1986","unstructured":"Lorentz, G.G.: Bernstein Polynomials, 2nd edn. Chelsea Publishing Company, New York, N.Y. (1986)","edition":"2"},{"issue":"1","key":"9256_CR25","doi-asserted-by":"crossref","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":"9256_CR26","doi-asserted-by":"crossref","unstructured":"McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) Proceedings of the 20th International Conference on Automated Deduction, proceedings. Lecture Notes in Computer Science, vol. 3632, pp. 295\u2013314 (2005)","DOI":"10.1007\/11532231_22"},{"key":"9256_CR27","doi-asserted-by":"crossref","unstructured":"Melquiond, G.: Proving bounds on real-valued functions with computations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12\u201315, 2008, Proceedings. Lecture Notes in Computer Science, vol. 5195, pp.\u00a02\u201317. Springer (2008). doi: 10.1007\/978-3-540-71070-7_2","DOI":"10.1007\/978-3-540-71070-7_2"},{"key":"9256_CR28","unstructured":"Moa, B.: Interval methods for global optimization. Ph.D. thesis, University of Victoria (2007)"},{"key":"9256_CR29","doi-asserted-by":"crossref","unstructured":"Monniaux, D., Corbineau, P.: On the generation of Positivstellensatz witnesses in degenerate cases. In: Proceedings of Interactive Theorem Proving (ITP). Lecture Notes in Computer Science (2011)","DOI":"10.1007\/978-3-642-22863-6_19"},{"key":"9256_CR30","unstructured":"Mu\u00f1oz, C., Mayero, M.: Real automation in the field. Tech. Rep. NASA\/CR-2001-211271 Interim ICASE Report No. 39, ICASE-NASA Langley, ICASE Mail Stop 132C, NASA Langley Research Center, Hampton VA 23681-2199, USA (2001)"},{"issue":"4","key":"9256_CR31","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/s11633-007-0342-7","volume":"4","author":"PSV Nataraj","year":"2007","unstructured":"Nataraj, P.S.V., Arounassalame, M.: A new subdivision algorithm for the Bernstein polynomial approach to global optimization. International Journal of Automation and Computing (IJAC) 4(4), 342\u2013352 (2007)","journal-title":"International Journal of Automation and Computing (IJAC)"},{"issue":"1","key":"9256_CR32","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1023\/A:1023061927787","volume":"9","author":"A Neumaier","year":"2003","unstructured":"Neumaier, A.: Taylor forms - use and limits. Reliab. Comput. 9(1), 43\u201379 (2003)","journal-title":"Reliab. Comput."},{"key":"9256_CR33","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) Proceeding of the 11th International Conference on Automated Deductioncade. Lecture Notes in Artificial Intelligence, vol.\u00a0607, pp.\u00a0748\u2013752. Springer (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"9256_CR34","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"PA Parrilo","year":"2003","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96, 293\u2013320 (2003). doi: 10.1007\/s10107-003-0387-5","journal-title":"Math. Program."},{"key":"9256_CR35","unstructured":"Passmore, G.O.: Combined decision procedures for nonlinear arithmetics, real and complex. Ph.D. thesis, The Univesity of Edinburgh (2011)"},{"key":"9256_CR36","doi-asserted-by":"crossref","unstructured":"Passmore, G.O., Jackson, P.B.: Combined decision techniques for the existential theory of the reals. In: Dixon, L. (ed.) Proceedings of Calculemus\/Mathematical Knowledge Managment. LNAI, pp. 122\u2013137, no. 5625.\u00a0Springer-Verlag (2009)","DOI":"10.1007\/978-3-642-02614-0_14"},{"key":"9256_CR37","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/s10898-008-9382-y","volume":"45","author":"S Ray","year":"2009","unstructured":"Ray, S., Nataraj, P.S.: An efficient algorithm for range computation of polynomials using the Bernstein form. J. Glob. Optim. 45, 403\u2013426 (2009)","journal-title":"J. Glob. Optim."},{"key":"9256_CR38","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1007\/s10898-007-9195-4","volume":"43","author":"AP Smith","year":"2009","unstructured":"Smith, A.P.: Fast construction of constant bound functions for sparse polynomials. J. Glob. Optim. 43, 445\u2013458 (2009)","journal-title":"J. Glob. Optim."},{"key":"9256_CR39","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. Univeristy of California Press (1951)","DOI":"10.1525\/9780520348097"},{"key":"9256_CR40","unstructured":"Verschelde, J.: The PHC pack, the database of polynomial systems. Tech. rep., Univeristy of Illinois, Mathematics Department, Chicago, IL (2001)"},{"key":"9256_CR41","doi-asserted-by":"crossref","unstructured":"Zippel, R.: Effective Polynomial Computation. Kluwer Academic Publishers (1993)","DOI":"10.1007\/978-1-4615-3188-3"},{"key":"9256_CR42","doi-asserted-by":"crossref","unstructured":"Zumkeller, R.: Formal global optimisation with Taylor models. In: Furbach, U., Shankar, N. (eds.) Proceedings of the Third International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science, vol.\u00a04130, pp.\u00a0408\u2013422 (2006)","DOI":"10.1007\/11814771_35"},{"key":"9256_CR43","unstructured":"Zumkeller, R.: Global Optimization in Type Theory. Ph.D. thesis, \u00c9cole Polytechnique Paris (2008)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9256-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9256-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9256-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,22]],"date-time":"2022-01-22T02:46:48Z","timestamp":1642819608000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9256-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,18]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["9256"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9256-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7,18]]}}}