{"id":865,"date":"2010-11-23T20:00:52","date_gmt":"2010-11-23T20:00:52","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=865"},"modified":"2013-03-08T05:50:07","modified_gmt":"2013-03-08T05:50:07","slug":"ra2010-ejercicios-de-razonamiento-proposicional-con-isabelle","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2010-ejercicios-de-razonamiento-proposicional-con-isabelle\/","title":{"rendered":"RA2010: Ejercicios de razonamiento proposicional con Isabelle"},"content":{"rendered":"<p> La clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\">Razonamiento autom\u00e1tico<\/a> ha consistido en la formalizaci\u00f3n en Isabelle\/Isar de demostraciones por deducci\u00f3n natural en l\u00f3gica proposicional. Para ello se han formalizado todas las demostraciones del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li\/temas\/tema-2.pdf\">tema de deducci\u00f3n natural proposicional<\/a> del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li\">L\u00f3gica inform\u00e1tica<\/a><\/p>\n<p>\nLas formalizaciones realizadas en clase se encuentran en el siguiente documento<br \/>\n<!--more--><br \/>\n\n<div class=\"gde-error\">GDE Error: Error al recuperar el fichero. Si es necesario, desactiva la comprobaci\u00f3n de errores (404:Not Found)<\/div>\n<\/p>\n<p>\nSe ha dejado como tarea para la pr\u00f3xima clase la formalizaci\u00f3n de las demostraiones del resto del tema y la soluci\u00f3n de los ejercicios de la <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\/ejercicios\/Relacion_1.pdf\">1\u00aa relaci\u00f3n<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>La clase de hoy del curso de Razonamiento autom\u00e1tico ha consistido en la formalizaci\u00f3n en Isabelle\/Isar de demostraciones por deducci\u00f3n natural en l\u00f3gica proposicional. Para ello se han formalizado todas las demostraciones del tema de deducci\u00f3n natural proposicional del curso de L\u00f3gica inform\u00e1tica Las formalizaciones realizadas en clase se encuentran en el siguiente documento<\/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":[145],"tags":[27,85,143],"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\/865"}],"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=865"}],"version-history":[{"count":9,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/865\/revisions"}],"predecessor-version":[{"id":2979,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/865\/revisions\/2979"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=865"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=865"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=865"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}