{"id":4728,"date":"2015-01-17T09:00:30","date_gmt":"2015-01-17T08:00:30","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4728"},"modified":"2015-01-17T08:10:34","modified_gmt":"2015-01-17T07:10:34","slug":"resena-formally-verified-decision-procedures-for-univariate-polynomial-computation-based-on-sturms-and-tarskis-theorems","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formally-verified-decision-procedures-for-univariate-polynomial-computation-based-on-sturms-and-tarskis-theorems\/","title":{"rendered":"Rese\u00f1a: Formally-verified decision procedures for univariate polynomial computation based on Sturm\u2019s and Tarski\u2019s theorems"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/pvs.csl.sri.com\">PVS<\/a> titulado <a href=\"http:\/\/shemesh.larc.nasa.gov\/people\/cam\/publications\/jar-nmd-2015-draft.pdf\">Formally-verified decision procedures for univariate polynomial computation based on Sturm\u2019s and Tarski\u2019s theorems<\/a><\/p>\n<p>Sus autores son <a href=\"http:\/\/shemesh.larc.nasa.gov\/people\/ajn\">Anthony Narkawicz<\/a>, <a href=\"http:\/\/shemesh.larc.nasa.gov\/people\/cam\">C\u00e9sar Mu\u00f1oz<\/a> y <a href=\"http:\/\/shemesh.larc.nasa.gov\/people\/amd\">Aaron M. Dutle<\/a> (del <a href=\"http:\/\/shemesh.larc.nasa.gov\/fm\/index.html\">Formal Methods group<\/a> en el <em>NASA Langley Research Center<\/em>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  <a href=\"http:\/\/en.wikipedia.org\/wiki\/Sturm%27s_theorem\">Sturm\u2019s theorem<\/a> is a well-known result in real algebraic geometry that provides a function that computes the number of roots of a univariate polynomial in a semi-open interval, not counting multiplicity. A generalization of Sturm\u2019s theorem is known as Tarski\u2019s theorem, which provides a linear relationship between functions known as Tarski queries and cardinalities of certain sets. The linear system that results from this relationship is in fact invertible and can be used to explicitly count the number of roots of a univariate polynomial on a set defined by a system of polynomial relations. This paper presents a formalization of these results in the PVS theorem prover, including formal proofs of Sturm\u2019s and Tarski\u2019s theorems. These theorems are at the basis of two decision procedures, which are implemented as computable functions in PVS. The first, based on Sturm\u2019s theorem, determines satisfiability of a single polynomial relation over an interval. The second, based on Tarski\u2019s theorem, determines the satisfiability of a system of polynomial relations over the real line. The soundness and completeness properties of these decision procedures are formally verified in PVS. The procedures and their correctness properties enable the implementation of PVS strategies for automatically proving existential and universal statements on polynomial systems. Since the decision procedures are formally verified in PVS, the soundness of the strategies depends solely on the internal logic of PVS rather than on an external oracle.\n<\/p><\/blockquote>\n<p>El trabajo se publicar\u00e1 en el <a href=\"http:\/\/bit.ly\/1yuuqwM\">Journal of Automated Reasoning<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en PVS del teorema de Sturm se encuentra <a href=\"http:\/\/shemesh.larc.nasa.gov\/people\/cam\/Sturm\">aqu\u00ed<\/a> y el del teorema de Tarski <a href=\"http:\/\/shemesh.larc.nasa.gov\/people\/cam\/Tarski\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en PVS titulado Formally-verified decision procedures for univariate polynomial computation based on Sturm\u2019s and Tarski\u2019s theorems Sus autores son Anthony Narkawicz, C\u00e9sar Mu\u00f1oz y Aaron M. Dutle (del Formal Methods group en el NASA Langley Research Center). Su resumen es Sturm\u2019s theorem is a well-known result in&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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":[100],"tags":[277,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\/4728"}],"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=4728"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4728\/revisions"}],"predecessor-version":[{"id":4729,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4728\/revisions\/4729"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4728"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4728"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4728"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}