{"id":1457,"date":"2011-07-22T16:54:13","date_gmt":"2011-07-22T16:54:13","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1457"},"modified":"2011-08-17T06:29:52","modified_gmt":"2011-08-17T06:29:52","slug":"resena-automated-theorem-provers-a-practical-tool-for-the-working-mathematician","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-automated-theorem-provers-a-practical-tool-for-the-working-mathematician\/","title":{"rendered":"Rese\u00f1a – Automated theorem provers: a practical tool for the working mathematician?"},"content":{"rendered":"

El art\u00edculo Automated theorem provers: a practical tool for the working mathematician?<\/a> de Alan Bundy<\/a> se ha publicado el 16 de julio en Annals of Mathematics and Artificial Intelligence<\/a>.<\/p>\n

En el art\u00edculo se analiza la utilizaci\u00f3n de los sistemas de demostraci\u00f3n asistida por ordenador (SDAO) en la investigaci\u00f3n matem\u00e1tica. Se parte del hecho de que los SDAO se usa por los matem\u00e1ticos menos que otros sistemas inform\u00e1ticos (como LaTeX o los sistemas de c\u00e1lculo simb\u00f3lico). Pero, su inter\u00e9s ha aumentado en la \u00faltima d\u00e9cada, como puede observarse en el n\u00famero de Diciembre de 2008 de las Notices of the AMS<\/a> dedicado a las demostraciones formales. El autor conjetura que este inter\u00e9s seguir\u00e1 creciendo e influir\u00e1 en la metodolog\u00eda matem\u00e1tica.<\/p>\n

Entre las causas de este creciente inter\u00e9s destaca la aparici\u00f3n de teoremas con grandes demostraciones (como el teorema de los cuatros colores<\/a>, la conjetura de Kepler<\/a> y la clasificaci\u00f3n de los grupos finitos<\/a>) en cuya demostraci\u00f3n se ha usado ordenadores. Se ha cr\u00edticado el uso de los ordenadores en la demostraci\u00f3n, por la posibilidad de que los programas tuviesen errores. Para asegurar su correcci\u00f3n se ha formalizado (en el caso del teorema de los cuatro colores) o se est\u00e1 formalizando (en los otros dos) su demostraci\u00f3n mediante SDAO.<\/p>\n

Otros razones para el aumento del inter\u00e9s en los SDAO se encuentra en nuevas aplicaciones como s\u00edntesis autom\u00e1tica de teoremas, automatizaci\u00f3n de la refactorizaci\u00f3n de demostraciones, b\u00fasqueda de teoremas, automatizaci\u00f3n de la revisi\u00f3n de art\u00edculos y automatizaci\u00f3n de la correcci\u00f3n de ex\u00e1menes.<\/p>\n

Por otra parte, entre las razones para la resistencia del uso de los SDAO y sus posibles soluciones, apunta las siguientes:<\/p>\n

    \n
  1. Las demostraciones formalizadas son demasiadas detalladas y largas<\/i>. Se puede mejorar presentando las demostraciones jar\u00e1rquicamente de forma que se pueda elegir el nivel de detalle y los pasos esenciales de las pruebas.<\/li>\n
  2. Los demostradores no son lo sufientemente potentes<\/i>. La potencia de los demostradores est\u00e1 creciendo as\u00ed como el volumen de matem\u00e1ticas formalizada.<\/li>\n
  3. Los demostradores son dif\u00edciles de usar<\/i>. Los desarrolladores de los sistemas est\u00e1n mejorando los interfaces. Una mejora significativa es el uso de demostraciones declarativas (como en Isar).\n<\/ol>\n

    Personalmente, pienso que la principal barrera est\u00e1 en disponer de una buena base de conocimiento formalizado utilizable en distintos SDAO y de herramientas de b\u00fasqueda sem\u00e1ntica en dicha base de conocimiento. Adem\u00e1s, entre las posibles aplicaciones de los SDAO creo que tambi\u00e9n ser\u00e1 importante su uso como ayudantes en la docencia como describe Benjamin C. Pierce en Using a Proof Assistant to Teach Programming Language Foundations<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"

    El art\u00edculo Automated theorem provers: a practical tool for the working mathematician? de Alan Bundy se ha publicado el 16 de julio en Annals of Mathematics and Artificial Intelligence. En el art\u00edculo se analiza la utilizaci\u00f3n de los sistemas de demostraci\u00f3n asistida por ordenador (SDAO) en la investigaci\u00f3n matem\u00e1tica. Se parte del hecho de que…<\/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":[166],"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\/1457"}],"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=1457"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1457\/revisions"}],"predecessor-version":[{"id":1510,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1457\/revisions\/1510"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1457"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1457"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1457"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}