{"id":164,"date":"2010-01-28T12:35:19","date_gmt":"2010-01-28T12:35:19","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=164"},"modified":"2013-03-08T05:53:47","modified_gmt":"2013-03-08T05:53:47","slug":"razonamiento-formalizado-en-analisis-numerico","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/razonamiento-formalizado-en-analisis-numerico\/","title":{"rendered":"Razonamiento formalizado en an\u00e1lisis num\u00e9rico"},"content":{"rendered":"<p>Hoy se ha publicado en arXiv el art\u00edculo <a href=\"http:\/\/arxiv.org\/abs\/1001.4898\">Formal Proof of a Wave Equation Resolution Scheme: the Method Error<\/a> escrito por Sylvie Boldo (INRIA Saclay &#8211; Ile de France, LRI), Francois Clement (INRIA Rocquencourt), Jean-Christophe Filli\u00e2tre (INRIA Saclay &#8211; Ile de France, LRI), Micaela Mayero (LIPN, INRIA Rh\u00f4ne-Alpes \/ LIP Laboratoire de l&#8217;Informatique du Parall\u00e9lisme), Guillaume Melquiond (INRIA Saclay &#8211; Ile de France, LRI) y Pierre Weis (INRIA Rocquencourt).<\/p>\n<p>En este trabajo se presenta una <a href=\"http:\/\/fost.saclay.inria.fr\/wave_method_error.php\">formalizaci\u00f3n en Coq<\/a> de una parte del conocimiento matem\u00e1tico m\u00e1s usado en las ingenier\u00eda: las ecuaciones diferenciales. Curiosamente las ecuaciones diferenciales apenas se han tratado dentro del razonamiento formalizado.<\/p>\n<p><!--more--><br \/>\nUno de los objetivos del trabajo es favorecer el uso de los m\u00e9todos formales en el an\u00e1lisis num\u00e9rico. Aunque pueda parecer una quimera, es una necesidad en matem\u00e1ticas aplicadas.<\/p>\n<p>Entre las conclusiones del trabajo destaco las siguientes:<\/p>\n<ol>\n<li> Algunas demostraciones usuales son superficiles, ya que no precisan las hip\u00f3tesis necesarias y suelen tener lagunas.\n<li> Para llenar las lagunas hay que generalizar los teoremas y masajear las demostraciones.\n<li> La formalizaci\u00f3n del razonamiento requiere mucho trabajo: la formalizaci\u00f3n del trabajo tiene 4.500 l\u00edneas de c\u00f3digo, una demostraci\u00f3n usual ocupa 10 p\u00e1ginas y una detallada ocupa 60 p\u00e1ginas. La formalizada es equivalente a la detallada.\n<li> La mitad del trabajo forma librer\u00edas reutilizables en otras formalizaciones.\n<\/ol>\n<p>Un estudio detallado del este art\u00edculo y la formalizaci\u00f3n podr\u00eda ser expuesto en el <a href=\"http:\/\/tinyurl.com\/yds6ot5\">Seminario del Grupo de L\u00f3gica Computacional<\/a>.<\/p>\n<p>Tambi\u00e9n ser\u00eda interesante estudiar c\u00f3mo formalizar el an\u00e1lisis num\u00e9rico en los sistemas que utilizamos en <a href=\"https:\/\/www.glc.us.es\">nuestro grupo<\/a> (ACL2, PVS, Isabelle\/Isar).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Hoy se ha publicado en arXiv el art\u00edculo Formal Proof of a Wave Equation Resolution Scheme: the Method Error escrito por Sylvie Boldo (INRIA Saclay &#8211; Ile de France, LRI), Francois Clement (INRIA Rocquencourt), Jean-Christophe Filli\u00e2tre (INRIA Saclay &#8211; Ile de France, LRI), Micaela Mayero (LIPN, INRIA Rh\u00f4ne-Alpes \/ LIP Laboratoire de l&#8217;Informatique du Parall\u00e9lisme),&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"closed","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":[46,20,45,89,271,273,44],"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\/164"}],"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=164"}],"version-history":[{"count":7,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/164\/revisions"}],"predecessor-version":[{"id":3075,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/164\/revisions\/3075"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=164"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=164"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=164"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}