Formalization of Bernstein polynomials and applications to global optimization. (English) Zbl 1314.68286

Muñoz, César; Narkawicz, Anthony

J. Autom. Reasoning 51, No. 2, 151-196 (2013).

Summary: 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.

MSC:

68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
65K10	Numerical optimization and variational techniques

Keywords:

formal verification; non-linear arithmetic; global optimization; Bernstein polynomials; interactive theorem proving

Software:

Database of Polynomial Systems; Coq; PVS; MetiTarski; ACL2; Gappa; RealPaver; Manip

References:

[1]	Akbarpour, B; Paulson, LC, Metitarski: an automatic theorem prover for real-valued special functions, J. Autom. Reason., 44, 175-205, (2010) · Zbl 1215.68206
[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) · Zbl 1071.65070
[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)
[4]	Bertot, Y., Guilhot, F., Mahboubi, A.: A formal study of Bernstein coefficients and polynomials. Tech. Rep. INRIA-005030117, INRIA (2010) · Zbl 1236.33016
[5]	Brisebarre, N; Joldes, M; Martin-Dorel, É; Mayero, M; Muller, JM; Pasca, I; Rideau, L; Théry, L; Goodloe, A (ed.); Person, S (ed.), Rigorous polynomial approximation using Taylor models in coq, 85-99, (2012), Norfolk, US
[6]	de Casteljau, P.: Formes à pôles. Hermès (1985) · Zbl 0655.41001
[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) · Zbl 1043.14018
[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-40, (2012) · Zbl 1241.68096
[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) · Zbl 1121.03023
[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) · Zbl 1346.65020
[11]	Daumas, M; Lester, D; Muñoz, C, Verified real number calculations: a library for interval arithmetic, IEEE Trans. Comput., 58, 1-12, (2009) · Zbl 1367.65213
[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)
[13]	Di Vito, B.: Manip user’s guide, version 1.3. Technical Memorandum NASA/TM-2002-211647, NASA Langley Research Center (2002) · Zbl 1191.90046
[14]	Dinechin, F; Lauter, C; Melquiond, G, Certifying the floating-point implementation of an elementary function using gappa, IEEE Trans. Comput., 60, 242-253, (2011) · Zbl 1367.65250
[15]	Garloff, J, Convergent bounds for the range of multivariate polynomials, 37-56, (1985), London, UK
[16]	Garloff, J, The Bernstein algorithm, Interval Comput., 4, 154-168, (1993) · Zbl 0829.65017
[17]	Garloff, J, Application of Bernstein expansion to the solution of control problems, Reliab. Comput., 6, 303-320, (2000) · Zbl 0965.65095
[18]	Granvilliers, L; Benhamou, F, Realpaver: an interval solver using constraint satisfaction techniques, ACM Trans. Math. Softw., 32, 138-156, (2006) · Zbl 1346.65020
[19]	Harrison, J.: Metatheory and reflection in theorem proving: a survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995)
[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) · Zbl 1144.68357
[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) · Zbl 1179.68136
[22]	Kaltofen, EL; Li, B; Yang, Z; Zhi, L; Robbiano, L (ed.); Abbott, J (ed.), Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients, (2010), Vienna
[23]	Kuchar, J; Yang, L, A review of conflict detection and resolution modeling methods, IEEE Trans. Intell. Transp. Syst., 1, 179-189, (2000)
[24]	Lorentz, G.G.: Bernstein Polynomials, 2nd edn. Chelsea Publishing Company, New York, N.Y. (1986) · Zbl 0989.41504
[25]	Mahboubi, A, Implementing the cylindrical algebraic decomposition within the coq system, Math. Struct. Comput. Sci., 17, 99-127, (2007) · Zbl 1121.03023
[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) · Zbl 1135.03329
[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 · Zbl 1165.68464
[28]	Moa, B.: Interval methods for global optimization. Ph.D. thesis, University of Victoria (2007) · Zbl 1241.68096
[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) · Zbl 1342.68296
[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) · Zbl 0829.65017
[31]	Nataraj, PSV; Arounassalame, M, A new subdivision algorithm for the Bernstein polynomial approach to global optimization, International Journal of Automation and Computing (IJAC), 4, 342-352, (2007)
[32]	Neumaier, A, Taylor forms - use and limits, Reliab. Comput., 9, 43-79, (2003) · Zbl 1071.65070
[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)
[34]	Parrilo, PA, Semidefinite programming relaxations for semialgebraic problems, Math. Program., 96, 293-320, (2003) · Zbl 1043.14018
[35]	Passmore, G.O.: Combined decision procedures for nonlinear arithmetics, real and complex. Ph.D. thesis, The Univesity of Edinburgh (2011)
[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) · Zbl 1247.03018
[37]	Ray, S; Nataraj, PS, An efficient algorithm for range computation of polynomials using the Bernstein form, J. Glob. Optim., 45, 403-426, (2009) · Zbl 1191.90046
[38]	Smith, AP, Fast construction of constant bound functions for sparse polynomials, J. Glob. Optim., 43, 445-458, (2009) · Zbl 1168.90011
[39]	Tarski, A.: A Decision Method for Elementary Algebra and Geometry. Univeristy of California Press (1951) · Zbl 0044.25102
[40]	Verschelde, J.: The PHC pack, the database of polynomial systems. Tech. rep., Univeristy of Illinois, Mathematics Department, Chicago, IL (2001)
[41]	Zippel, R.: Effective Polynomial Computation. Kluwer Academic Publishers (1993) · Zbl 0794.11048
[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) · Zbl 1222.68377
[43]	Zumkeller, R.: Global Optimization in Type Theory. Ph.D. thesis, École Polytechnique Paris (2008)