Journal of Automated Reasoning

, Volume 51, Issue 2, pp 151–196 | Cite as

Formalization of Bernstein Polynomials and Applications to Global Optimization

  • César Muñoz
  • Anthony Narkawicz


This paper presents a formalization in higher-order logic of a practical representation of multivariate Bernstein polynomials. Using this representation, an algorithm for finding lower and upper bounds of the minimum and maximum values of a polynomial has been formalized and verified correct in the Prototype Verification System (PVS). The algorithm is used in the definition of proof strategies for formally and automatically solving polynomial global optimization problems.


Formal verification Non-linear arithmetic Global optimization Bernstein polynomials Interactive theorem proving 


  1. 1.
    Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175–205 (2010)MathSciNetMATHCrossRefGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Archer, M., Di Vito, B., Muñoz, 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)Google Scholar
  4. 4.
    Bertot, Y., Guilhot, F., Mahboubi, A.: A formal study of Bernstein coefficients and polynomials. Tech. Rep. INRIA-005030117, INRIA (2010)Google Scholar
  5. 5.
    Brisebarre, N., Joldes, M., Martin-Dorel, É., Mayero, M., Muller, J.M., Pasca, I., Rideau, L., Théry, 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–99. Springer, Norfolk, US (2012)Google Scholar
  6. 6.
    de Casteljau, P.: Formes à pôles. Hermès (1985)Google Scholar
  7. 7.
    Cháves, F., Daumas, M.: A library of Taylor models for PVS automatic proof checker. Technical Report RR2006-07, École Normale Supérieure de Lyon (2006)Google Scholar
  8. 8.
    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–40 (2012)MathSciNetGoogle Scholar
  9. 9.
    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. 33, pp. 134–183. Springer, Kaiserslautern (1975)Google Scholar
  10. 10.
    Crespo, L.G., Muñoz, 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)Google Scholar
  11. 11.
    Daumas, M., Lester, D., Muñoz, C.: Verified real number calculations: a library for interval arithmetic. IEEE Trans. Comput. 58(2), 1–12 (2009)CrossRefGoogle Scholar
  12. 12.
    Delahaye, D., Mayero, M.: Field, une procédure de décision pour les nombres réels en coq. In: Castéran, P. (ed.) Journées Francophones des Langages Applicatifs (JFLA’01), pp. 33–48. Collection Didactique, INRIA, Pontarlier, France, Janvier (2001)Google Scholar
  13. 13.
    Di Vito, B.: Manip user’s guide, version 1.3. Technical Memorandum NASA/TM-2002-211647, NASA Langley Research Center (2002)Google Scholar
  14. 14.
    de Dinechin, F., Lauter, C., Melquiond, G.: Certifying the floating-point implementation of an elementary function using Gappa. IEEE Trans. Comput. 60(2), 242–253 (2011)MathSciNetCrossRefGoogle Scholar
  15. 15.
    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–56. Springer-Verlag, London, UK (1985)Google Scholar
  16. 16.
    Garloff, J.: The Bernstein algorithm. Interval Comput. 4, 154–168 (1993)MathSciNetGoogle Scholar
  17. 17.
    Garloff, J.: Application of Bernstein expansion to the solution of control problems. Reliab. Comput. 6, 303–320 (2000)MathSciNetMATHCrossRefGoogle Scholar
  18. 18.
    Granvilliers, L., Benhamou, F.: RealPaver: an interval solver using constraint satisfaction techniques. ACM Trans. Math. Softw. 32(1), 138–156 (2006)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Harrison, J.: Metatheory and reflection in theorem proving: a survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995)Google Scholar
  20. 20.
    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–118. Springer (2007)Google Scholar
  21. 21.
    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–333. Springer, L’Aquila, Italy (2003)Google Scholar
  22. 22.
    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)Google Scholar
  23. 23.
    Kuchar, J., Yang, L.: A review of conflict detection and resolution modeling methods. IEEE Trans. Intell. Transp. Syst. 1(4), 179–189 (2000)CrossRefGoogle Scholar
  24. 24.
    Lorentz, G.G.: Bernstein Polynomials, 2nd edn. Chelsea Publishing Company, New York, N.Y. (1986)MATHGoogle Scholar
  25. 25.
    Mahboubi, A.: Implementing the cylindrical algebraic decomposition within the Coq system. Math. Struct. Comput. Sci. 17(1), 99–127 (2007)MathSciNetMATHCrossRefGoogle Scholar
  26. 26.
    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–314 (2005)Google Scholar
  27. 27.
    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–15, 2008, Proceedings. Lecture Notes in Computer Science, vol. 5195, pp. 2–17. Springer (2008). doi: 10.1007/978-3-540-71070-7_2
  28. 28.
    Moa, B.: Interval methods for global optimization. Ph.D. thesis, University of Victoria (2007)Google Scholar
  29. 29.
    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)Google Scholar
  30. 30.
    Muñoz, 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)Google Scholar
  31. 31.
    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–352 (2007)CrossRefGoogle Scholar
  32. 32.
    Neumaier, A.: Taylor forms - use and limits. Reliab. Comput. 9(1), 43–79 (2003)MathSciNetMATHCrossRefGoogle Scholar
  33. 33.
    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. 607, pp. 748–752. Springer (1992)Google Scholar
  34. 34.
    Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96, 293–320 (2003). doi: 10.1007/s10107-003-0387-5 MathSciNetMATHCrossRefGoogle Scholar
  35. 35.
    Passmore, G.O.: Combined decision procedures for nonlinear arithmetics, real and complex. Ph.D. thesis, The Univesity of Edinburgh (2011)Google Scholar
  36. 36.
    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–137, no. 5625. Springer-Verlag (2009)Google Scholar
  37. 37.
    Ray, S., Nataraj, P.S.: An efficient algorithm for range computation of polynomials using the Bernstein form. J. Glob. Optim. 45, 403–426 (2009)MathSciNetMATHCrossRefGoogle Scholar
  38. 38.
    Smith, A.P.: Fast construction of constant bound functions for sparse polynomials. J. Glob. Optim. 43, 445–458 (2009)MATHCrossRefGoogle Scholar
  39. 39.
    Tarski, A.: A Decision Method for Elementary Algebra and Geometry. Univeristy of California Press (1951)Google Scholar
  40. 40.
    Verschelde, J.: The PHC pack, the database of polynomial systems. Tech. rep., Univeristy of Illinois, Mathematics Department, Chicago, IL (2001)Google Scholar
  41. 41.
    Zippel, R.: Effective Polynomial Computation. Kluwer Academic Publishers (1993)Google Scholar
  42. 42.
    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. 4130, pp. 408–422 (2006)Google Scholar
  43. 43.
    Zumkeller, R.: Global Optimization in Type Theory. Ph.D. thesis, École Polytechnique Paris (2008)Google Scholar

Copyright information

© © Springer Science+Business Media B.V. (outside the USA) 2012

Authors and Affiliations

  1. 1.NASA Langley Research CenterHamptonUSA

Personalised recommendations