{"id":1159,"date":"2011-01-18T08:48:47","date_gmt":"2011-01-18T08:48:47","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1159"},"modified":"2013-03-08T05:50:03","modified_gmt":"2013-03-08T05:50:03","slug":"ra2010-patrones-de-demostracion-y-heuristica-de-generalizacion-en-isabelle","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2010-patrones-de-demostracion-y-heuristica-de-generalizacion-en-isabelle\/","title":{"rendered":"RA2010: Patrones de demostraci\u00f3n y heur\u00edstica de generalizaci\u00f3n en Isabelle"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\">Razonamiento autom\u00e1tico<\/a> se han presentado los patrones fundamentales de demostraci\u00f3n en Isabelle. En concreto, se han estudiado las demostraciones por casos, con negaciones, por contradicci\u00f3n, con equivalencias. Tambi\u00e9n se ha estudiado la heur\u00edstica de generalizaci\u00f3n en las demostraciones por inducci\u00f3n.<\/p>\n<p>Las transparencias usadas en clase son las p\u00e1ginas 35-39 del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-10\/temas\/tema-4.pdf\">tema 4<\/a> y las p\u00e1ginas 40-43 del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-10\/temas\/tema-5.pdf\">tema 5<\/a>.<\/p>\n<p>El c\u00f3digo correspondiente se encuentra en <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\/temas\/Cap_4.thy\">Cap_4.thy<\/a> y <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\/temas\/Cap_5.thy\">Cap_5.thy<\/a>. <\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se han presentado los patrones fundamentales de demostraci\u00f3n en Isabelle. En concreto, se han estudiado las demostraciones por casos, con negaciones, por contradicci\u00f3n, con equivalencias. Tambi\u00e9n se ha estudiado la heur\u00edstica de generalizaci\u00f3n en las demostraciones por inducci\u00f3n. Las transparencias usadas en clase son las&#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":[145],"tags":[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\/1159"}],"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=1159"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1159\/revisions"}],"predecessor-version":[{"id":2945,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1159\/revisions\/2945"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1159"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1159"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1159"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}