{"id":2088,"date":"2012-07-22T05:57:27","date_gmt":"2012-07-22T05:57:27","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2088"},"modified":"2013-03-08T05:48:14","modified_gmt":"2013-03-08T05:48:14","slug":"resena-formalization-of-an-efficient-representation-of-bernstein-polynomials-and-applications-to-global-optimization","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formalization-of-an-efficient-representation-of-bernstein-polynomials-and-applications-to-global-optimization\/","title":{"rendered":"Rese\u00f1a: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization"},"content":{"rendered":"<p>Esta semana se ha publicado en el Journal of Automated Reasoning un nuevo art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/pvs.csl.sri.com\/\">PVS<\/a>: <a href=\"http:\/\/www.springerlink.com\/content\/8g508865h3t35632\/\">Formalization of an efficient representation of Bernstein polynomials and applications to global optimization<\/a>. Una versi\u00f3n previa se puede leer libremente <a href=\"http:\/\/shemesh.larc.nasa.gov\/people\/cam\/Bernstein\/bernstein.pdf\">aqu\u00ed<\/a>. <\/p>\n<p>Los autores son <a href=\"http:\/\/shemesh.larc.nasa.gov\/people\/cam\/\">C\u00e9sar Mu\u00f1oz<\/a> y <a href=\"http:\/\/shemesh.larc.nasa.gov\/people\/ajn\/\">Anthony Narkawicz<\/a> de <a href=\"http:\/\/shemesh.larc.nasa.gov\/fm\/\">NASA Langley Formal Methods<\/a>.<\/p>\n<p>Su resumen es <\/p>\n<blockquote><p>\nThis 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.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana se ha publicado en el Journal of Automated Reasoning un nuevo art\u00edculo de razonamiento formalizado en PVS: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization. Una versi\u00f3n previa se puede leer libremente aqu\u00ed. Los autores son C\u00e9sar Mu\u00f1oz y Anthony Narkawicz de NASA Langley Formal Methods. Su resumen&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[277,273,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2088"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=2088"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2088\/revisions"}],"predecessor-version":[{"id":2807,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2088\/revisions\/2807"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2088"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2088"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2088"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}