{"id":1472,"date":"2011-07-29T06:01:00","date_gmt":"2011-07-29T06:01:00","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1472"},"modified":"2011-07-29T06:01:00","modified_gmt":"2011-07-29T06:01:00","slug":"interactive-proof-introduction-to-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/interactive-proof-introduction-to-isabellehol\/","title":{"rendered":"Interactive Proof: Introduction to Isabelle\/HOL"},"content":{"rendered":"<p><a href=\"http:\/\/www4.in.tum.de\/~nipkow\/\">Tobias Nipkow<\/a> ha publicado un nuevo tutorial de Isabell\/HOL: <a href=\"http:\/\/www4.in.tum.de\/~nipkow\/MOD2011\/isabelle-notes.pdf\">Interactive Proof: Introduction to Isabelle\/HOL<\/a>, que presentar\u00e1 a principio de agosto en la <a href=\"http:\/\/asimod.in.tum.de\">Summer School Marktoberdorf 2011<\/a>.<\/p>\n<p>El contenido del tutorial es el siguiente:<\/p>\n<ul>\n<li><i>Elementos b\u00e1sicos de Isabelle\/HOL<\/i>: los tipos, t\u00e9rminos, f\u00f3rmulas y teor\u00edas.<\/li>\n<li><i>Isabelle\/HOL como lenguaje funcional verificable<\/i>. En esta secci\u00f3n, presenta los tipos b\u00e1sicos (bool, nat y list), c\u00f3mo pueden definirse funciones y tipos y c\u00f3mo pueden demostrarse propiedades por inducci\u00f3n y simplificaci\u00f3n.<\/li>\n<li><i>L\u00f3gica y automatizaci\u00f3n de las demostraciones<\/i>. En esta secci\u00f3n, presenta c\u00f3mo se trabaja con f\u00f3rmulas y conjuntos, c\u00f3mo puede automatizarse las demostraciones de sus propiedades y c\u00f3mo pueden analizarse las demostraciones en pasos elementales.<\/li>\n<li><i>Demostraciones estructuradas con Isar<\/i>. En esta secci\u00f3n, presenta ejemplos de demostraciones en Isar, patrones de demostraciones, t\u00e9cnicas para mejorar demostraciones y demostraciones por inducci\u00f3n y casos en Isar.<\/li>\n<\/ul>\n<p>La presentaci\u00f3n del tutorial est\u00e1 <i>basada en ejemplos<\/i>: se concentra en ejemplos que presenta los casos t\u00edpicos sin explicar el caso general si se puede inferir de los ejemplos.<\/p>\n<p>Las teor\u00edas que sirven de ejemplo del tutorial son las siguientes: <a href=\"http:\/\/www4.informatik.tu-muenchen.de\/lehre\/vorlesungen\/perlen\/SS11\/Isabelle\/Overview_Demo.thy\">Overview<\/a>, <a href=\"http:\/\/www4.informatik.tu-muenchen.de\/lehre\/vorlesungen\/perlen\/SS11\/Isabelle\/Nat_Demo.thy\">Nat<\/a>, <a href=\"http:\/\/www4.informatik.tu-muenchen.de\/lehre\/vorlesungen\/perlen\/SS11\/Isabelle\/List_Demo.thy\">List<\/a>, <a href=\"http:\/\/www4.informatik.tu-muenchen.de\/lehre\/vorlesungen\/perlen\/SS11\/Isabelle\/Tree_Demo.thy\">Tree<\/a>, <a href=\"http:\/\/www4.informatik.tu-muenchen.de\/lehre\/vorlesungen\/perlen\/SS11\/Isabelle\/Simp_Demo.thy\">Simp<\/a>, <a href=\"http:\/\/www4.informatik.tu-muenchen.de\/lehre\/vorlesungen\/perlen\/SS11\/Isabelle\/Induct_Demo.thy\">Induct<\/a>, <a href=\"http:\/\/www4.informatik.tu-muenchen.de\/lehre\/vorlesungen\/perlen\/SS11\/Isabelle\/Auto_Proof_Demo.thy\">Auto_Proof_Demo<\/a>, <a href=\"http:\/\/www4.informatik.tu-muenchen.de\/lehre\/vorlesungen\/perlen\/SS11\/Isabelle\/Single_Step_Demo.thy\">Single_Step_Demo<\/a>, <a href=\"http:\/\/www4.informatik.tu-muenchen.de\/lehre\/vorlesungen\/perlen\/SS11\/Isabelle\/Inductive_Demo.thy\">Inductive_Demo<\/a>, <a href=\"http:\/\/www4.informatik.tu-muenchen.de\/lehre\/vorlesungen\/perlen\/SS11\/Isabelle\/Isar_Demo.thy\">Isar_Demo<\/a>, <a href=\"http:\/\/www4.informatik.tu-muenchen.de\/lehre\/vorlesungen\/perlen\/SS11\/Isabelle\/Isar_Induct_Demo.thy\">Isar_Induct_Demo<\/a>.<\/p>\n<p>El resto del material utilizado se encuentra en <a href=\"http:\/\/www4.in.tum.de\/~nipkow\/MOD2011\">MOD2011<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tobias Nipkow ha publicado un nuevo tutorial de Isabell\/HOL: Interactive Proof: Introduction to Isabelle\/HOL, que presentar\u00e1 a principio de agosto en la Summer School Marktoberdorf 2011. El contenido del tutorial es el siguiente: Elementos b\u00e1sicos de Isabelle\/HOL: los tipos, t\u00e9rminos, f\u00f3rmulas y teor\u00edas. Isabelle\/HOL como lenguaje funcional verificable. En esta secci\u00f3n, presenta los tipos b\u00e1sicos&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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":[100],"tags":[144,148,163,285,176],"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\/1472"}],"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=1472"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1472\/revisions"}],"predecessor-version":[{"id":1475,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1472\/revisions\/1475"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1472"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1472"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1472"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}