Esta entrada est\u00e1 dedicada a los antecentes de la certificaci\u00f3n computacional del conocimiento matem\u00e1tico en estilo declarativo.<\/p>\n
Por lo que respecta a la verificaci\u00f3n declarativa, sus raices se encuentran en el trabajo realizado en el proyecto Mizar<\/a>. El proyecto Mizar comenz\u00f3 en el 1973 como un intento de reconstruir la matem\u00e1tica en un entorno computacionalmente certificable. Los teoremas demostrados dentro del proyecto Mizar se encuentran fundamentalmente en la Mizar Mathematical Library<\/a> y en la revista Formalized Mathematics<\/a> que se publica desde el a\u00f1o 1990. El sistema Mizar no es autom\u00e1tico sino que es s\u00f3lo un verificador. Por contra, los sistemas de demostraci\u00f3n no dispon\u00edan de modos de demostraci\u00f3n declararativa hasta que M. Wenzel cre\u00f3 Isar (Intelligible semi-automated reasoning)<\/a>. Isar est\u00e1 construido sobre el sistema Isabelle<\/a>. Isabelle es un asistente de prueba gen\u00e9rico desarrollado por L. Paulson (en la Universidad de Cambridge) y T. Nipkow (en la Universidad Polit\u00e9cnica de Munich). Las teor\u00edas formalizadas en Isabelle\/Isar se encuentran fundamentalmente en la biblioteca de Isabelle2009-1<\/a>, en la revista The Archive of Formal Proofs<\/a> y en la IsarMathLib (A library of formalized mathematics for Isabelle\/ZF theorem proving environment)<\/a>.<\/p>\n Por lo que respecta a la certificaci\u00f3n computacional del conocimiento Esta entrada est\u00e1 dedicada a los antecentes de la certificaci\u00f3n computacional del conocimiento matem\u00e1tico en estilo declarativo. Por lo que respecta a la verificaci\u00f3n declarativa, sus raices se encuentran en el trabajo realizado en el proyecto Mizar. El proyecto Mizar comenz\u00f3 en el 1973 como un intento de reconstruir la matem\u00e1tica en un entorno computacionalmente…<\/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":[6,8],"tags":[],"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\/167"}],"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=167"}],"version-history":[{"count":5,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/167\/revisions"}],"predecessor-version":[{"id":3074,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/167\/revisions\/3074"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=167"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=167"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=167"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
\nmatem\u00e1tico los antecedentes pueden situarse en el 1993 con la publicaci\u00f3n del manifiesto del proyecto QED<\/a> impulsado por Bob Boyer y la revisi\u00f3n del proyecto QED<\/a> en 2007 por F. Wiedijk. Actualmente se han demostrado muchos teoremas matem\u00e1ticos importantes, como puede comprobarse en Formalizing 100 Theorems<\/a>, en la NASA Langley PVS Libraries<\/a> y en The Coq Users’ Contributions<\/a>. Entre los teoremas formalmente certificados podemos citar el teorema de de la distribuci\u00f3n de los n\u00fameros primos<\/a>, el teorema de los cuatro colores<\/a> y el teorema de la curva de Jordan<\/a>. Nuestro grupo<\/a> posee experiencia en la certificaci\u00f3n de teoremas matem\u00e1ticos habiendo certificado en ACL2 y PVS, entre otros, el lema de Newman<\/a>, el teorema de Knuth-Bendix<\/a>, el teorema de correcci\u00f3n del algoritmo de Buchberger<\/a>, el teorema de Bezem de completitud de la resoluci\u00f3n proposicional<\/a> y el teorema de completitud de la resoluci\u00f3n SLD<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"