{"id":7229,"date":"2020-08-07T11:18:59","date_gmt":"2020-08-07T09:18:59","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7229"},"modified":"2020-08-29T11:25:47","modified_gmt":"2020-08-29T09:25:47","slug":"formatus-presentacion-de-dao-demostracion-asistida-por-ordenador-con-lean","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formatus-presentacion-de-dao-demostracion-asistida-por-ordenador-con-lean\/","title":{"rendered":"ForMatUS: Presentaci\u00f3n de &#8220;DAO (Demostraci\u00f3n Asistida por Ordenador) con Lean&#8221;"},"content":{"rendered":"<p>Dentro del <a href=\"https:\/\/bit.ly\/3bbGk6r\">proyecto ForMatUS<\/a> el primer subproyecto, titulado &#8220;DAO (Demostraci\u00f3n Asistida por Ordenador) con Lean&#8221; tiene como base la l\u00f3gica que se estudia en las asignaturas de<\/p>\n<ul>\n<li><a href=\"http:\/\/bit.ly\/39AasGL\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> de 3\u00ba del Grado en Matem\u00e1ticas.<\/li>\n<li><a href=\"https:\/\/bit.ly\/2QwwpyS\">L\u00f3gica inform\u00e1tica<\/a> de 2\u00ba del Grado en Ingenier\u00eda Inform\u00e1tica.<\/li>\n<li><a href=\"https:\/\/bit.ly\/3gAnUgJ\">Razonamiento autom\u00e1tico<\/a> del M\u00e1ster Universitario en L\u00f3gica, Computaci\u00f3n e Inteligencia Artificial. <\/li>\n<\/ul>\n<p>El objetivo concreto de este subproyecto es presentar una introducci\u00f3n a la DAO (Demostraci\u00f3n Asistida con Ordenador) usando <a href=\"https:\/\/leanprover.github.io\/\">Lean<\/a> para usarla en las clases de la asignatura de <a href=\"https:\/\/bit.ly\/3gAnUgJ\">Razonamiento autom\u00e1tico<\/a>. Por tanto, el \u00fanico prerrequisito es, como en el M\u00e1ster, cierta madurez matem\u00e1tica como la que deben tener los alumnos de los Grados de Matem\u00e1tica y de Inform\u00e1tica.<\/p>\n<p>La exposici\u00f3n se har\u00e1 mediante una colecci\u00f3n de ejercicios. En cada ejercicios se mostrar\u00e1n distintas pruebas del mismo resultado y se comentar\u00e1n las t\u00e1cticas conforme se van usando y los lemas utilizados en las demostraciones.<\/p>\n<p>Adem\u00e1s, para cada ejercicio se proporcionan tres enlaces:<\/p>\n<ul>\n<li>el primero, al c\u00f3digo comentado,<\/li>\n<li>el segundo, a Lean Web con el ejercicio para experimentar en el navegador, y<\/li>\n<li>el tercero. a un v\u00eddeo explicando las soluciones del ejercicio.<\/li>\n<\/ul>\n<p>El proyecto se desarrollar\u00e1 en<\/p>\n<ul>\n<li>el repositorio <a href=\"https:\/\/bit.ly\/34LaHzI\">DAO_con_Lean<\/a> de GitHub,<\/li>\n<li>el libro <a href=\"https:\/\/bit.ly\/2YKFHMg\">DAO (Demostraci\u00f3n Asistida por Ordenador) con Lean<\/a><\/li>\n<li>los v\u00eddeos de la lista <a href=\"https:\/\/bit.ly\/2QwnT30\">DAO (Demostraci\u00f3n Asistida por Ordenador) con Lean<\/a> de YouTube<\/li>\n<li>los mensajes en Twitter con la etiqueta <a href=\"https:\/\/bit.ly\/3lqzxKW\">#ForMatUS<\/a> y<\/li>\n<li>las entradas en este blog con la categor\u00eda <a href=\"https:\/\/bit.ly\/2QDT8Je\">ForMatUS<\/a>.<\/li>\n<\/ul>\n<p>En el siguiente v\u00eddeo se presenta el proyecto:<\/p>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/HHM1i-anf5s\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Dentro del proyecto ForMatUS el primer subproyecto, titulado &#8220;DAO (Demostraci\u00f3n Asistida por Ordenador) con Lean&#8221; tiene como base la l\u00f3gica que se estudia en las asignaturas de L\u00f3gica matem\u00e1tica y fundamentos de 3\u00ba del Grado en Matem\u00e1ticas. L\u00f3gica inform\u00e1tica de 2\u00ba del Grado en Ingenier\u00eda Inform\u00e1tica. Razonamiento autom\u00e1tico del M\u00e1ster Universitario en L\u00f3gica, Computaci\u00f3n e&#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":[335],"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\/7229"}],"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=7229"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7229\/revisions"}],"predecessor-version":[{"id":7232,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7229\/revisions\/7232"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7229"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7229"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7229"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}