{"id":374,"date":"2021-05-16T18:19:35","date_gmt":"2021-05-16T16:19:35","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=374"},"modified":"2021-08-21T13:19:30","modified_gmt":"2021-08-21T11:19:30","slug":"sobre-calculemus","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/sobre-calculemus\/","title":{"rendered":"Sobre Calculemus"},"content":{"rendered":"<p>El objetivo principal de <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\">Calculemus<\/a> es proponer ejercicios de demostraci\u00f3n de resultados matem\u00e1ticos usando <a href=\"https:\/\/bit.ly\/2RlLVli\">sistemas de demostraci\u00f3n interactiva<\/a>, fundamentalmente <a href=\"https:\/\/bit.ly\/3jTRgtf\">Lean<\/a> e <a href=\"https:\/\/bit.ly\/3uOgD4e\">Isabelle\/HOL<\/a>.<\/p>\n<p>En los enunciados de los ejercicios se da la plantilla para <a href=\"https:\/\/bit.ly\/3jTRgtf\">Lean<\/a>.<\/p>\n<p>Las soluciones propuestas est\u00e1n en la <a href=\"https:\/\/bit.ly\/34LOtMt\">versi\u00f3n 3.30.0 de Lean<\/a> y en la <a href=\"https:\/\/bit.ly\/3uOgD4e\">versi\u00f3n 2021 de Isabelle\/HOL<\/a>. Las distintas soluciones est\u00e1n ordenadas desde las m\u00e1s detalladas a las m\u00e1s autom\u00e1ticas. Adem\u00e1s, las soluciones est\u00e1n en <a href=\"https:\/\/bit.ly\/3gaKMFB\">este repositorio de GitHub<\/a>.<\/p>\n<p>Es recomendable, antes de leer las soluciones propuestas, intentar escribir demostraciones propias (en el caso de Lean se pueden probar en el navegador a trav\u00e9s de <a href=\"https:\/\/bit.ly\/3wRIsKk\">este enlace<\/a>).<\/p>\n<p>En los comentarios se pueden publicar demostraciones distintas de las propuestas en Lean, Isabelle\/HOL u otros sistemas (como <a href=\"https:\/\/bit.ly\/3uNqNC0\">Coq<\/a>, <a href=\"https:\/\/bit.ly\/34OeiLO\">Agda<\/a> o <a href=\"https:\/\/bit.ly\/2Sb9H3E\">PVS<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>El objetivo principal de Calculemus es proponer ejercicios de demostraci\u00f3n de resultados matem\u00e1ticos usando sistemas de demostraci\u00f3n interactiva, fundamentalmente Lean e Isabelle\/HOL. En los enunciados de los ejercicios se da la plantilla para Lean. Las soluciones propuestas est\u00e1n en la versi\u00f3n 3.30.0 de Lean y en la versi\u00f3n 2021 de Isabelle\/HOL. Las distintas soluciones est\u00e1n ordenadas desde las m\u00e1s detalladas a las m\u00e1s autom\u00e1ticas. Adem\u00e1s, las soluciones est\u00e1n en este repositorio de GitHub. Es recomendable, antes de leer las soluciones propuestas, intentar escribir demostraciones propias (en el caso de Lean se pueden probar en el navegador a trav\u00e9s de este enlace). En los comentarios se pueden publicar demostraciones distintas de las propuestas en Lean, Isabelle\/HOL u otros sistemas (como Coq, Agda o PVS.<\/p>\n","protected":false},"author":1,"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,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[107],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/374"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=374"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/374\/revisions"}],"predecessor-version":[{"id":375,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/374\/revisions\/375"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=374"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=374"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=374"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}