Reseña: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization

PorJosé A. Alonso

Esta semana se ha publicado en el Journal of Automated Reasoning un nuevo artículo de razonamiento formalizado en PVS: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization. Una versión previa se puede leer libremente aquí.

Los autores son César Muñoz y Anthony Narkawicz de NASA Langley Formal Methods.

Su resumen es

This paper presents a formalization in higher-order logic of an efficient 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.