{"id":1135,"date":"2011-01-11T07:21:09","date_gmt":"2011-01-11T07:21:09","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1135"},"modified":"2013-03-08T05:50:04","modified_gmt":"2013-03-08T05:50:04","slug":"ra2010-razonamiento-por-induccion-sobre-tipos-recursivos","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2010-razonamiento-por-induccion-sobre-tipos-recursivos\/","title":{"rendered":"RA2010: Razonamiento por inducci\u00f3n sobre tipos recursivos"},"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 las t\u00e9cnicas de demostraci\u00f3n en Isabelle por inducci\u00f3n sobre tipos recursivos. En concreto se han estudiado los esquemas de inducci\u00f3n para las listas y para los \u00e1rboles binarios. <\/p>\n<p>Las transparencias usadas en clase son las p\u00e1ginas 31-34 del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-10\/temas\/tema-3.pdf\">tema 3 (Distinci\u00f3n decasos e inducci\u00f3n)<\/a>. El c\u00f3digo correspondiente se encuentra en <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\/temas\/Cap_3.thy\">Cap_3.thy<\/a>. <\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se han presentado las t\u00e9cnicas de demostraci\u00f3n en Isabelle por inducci\u00f3n sobre tipos recursivos. En concreto se han estudiado los esquemas de inducci\u00f3n para las listas y para los \u00e1rboles binarios. Las transparencias usadas en clase son las p\u00e1ginas 31-34 del tema 3 (Distinci\u00f3n decasos&#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\/1135"}],"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=1135"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1135\/revisions"}],"predecessor-version":[{"id":2950,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1135\/revisions\/2950"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1135"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1135"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1135"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}