{"id":5356,"date":"2016-03-08T18:47:36","date_gmt":"2016-03-08T17:47:36","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5356"},"modified":"2016-03-10T11:48:37","modified_gmt":"2016-03-10T10:48:37","slug":"lmf2016-deduccion-natural-proposicional-en-isabellehol-2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2016-deduccion-natural-proposicional-en-isabellehol-2\/","title":{"rendered":"LMF2016: Deducci\u00f3n natural proposicional en Isabelle\/HOL (2)"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-15\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha continuado el estudio de la formalizaci\u00f3n en Isabelle\/HOL de las demostraciones por deducci\u00f3n natural estudiadas en el <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-15\/temas\/tema-2.pdf\">tema 2<\/a> iniciado en la clase anterior.<\/p>\n<p>Para cada uno de los ejemplos se ha presentado distintas demostraciones: detallada (que sea parecida a la mostrada en las transparencias), estructurada y autom\u00e1tica.<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nsubsection {* Reglas de la disyunci\u00f3n *}\n\ntext {*\n  Las reglas de la introducci\u00f3n de la disyunci\u00f3n son\n  \u00b7 disjI1: P \u27f9 P \u2228 Q\n  \u00b7 disjI2: Q \u27f9 P \u2228 Q\n  La regla de elimaci\u00f3n de la disyunci\u00f3n es\n  \u00b7 disjE:  \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R \n*}\n\ntext {* \n  Ejemplo 12 (p. 11). Demostrar\n     p \u2228 q \u22a2 q \u2228 p\n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_12_1:\n  assumes \"p \u2228 q\" \n  shows \"q \u2228 p\"\nproof -\n  have \"p \u2228 q\" using assms by this\n  moreover\n  { assume 2: \"p\"\n    have \"q \u2228 p\" using 2 by (rule disjI2) }\n  moreover\n  { assume 3: \"q\"\n    have \"q \u2228 p\" using 3 by (rule disjI1) }\n  ultimately show \"q \u2228 p\" by (rule disjE) \nqed    \n\ntext {*\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"moreover\" para separar los bloques y\n  \u00b7 \"ultimately\" para unir los resultados de los bloques. *}\n \n-- \"La demostraci\u00f3n detallada con reglas impl\u00edcitas es\"\nlemma ejemplo_12_2:\n  assumes \"p \u2228 q\" \n  shows \"q \u2228 p\"\nproof -\n  note `p \u2228 q`\n  moreover\n  { assume \"p\"\n    hence \"q \u2228 p\" .. }\n  moreover\n  { assume \"q\"\n    hence \"q \u2228 p\" .. }\n  ultimately show \"q \u2228 p\" ..\nqed    \n\ntext {*\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"note\" para copiar un hecho. *}\n\n-- \"La demostraci\u00f3n hacia atr\u00e1s es\"\nlemma ejemplo_12_3:\n  assumes 1: \"p \u2228 q\" \n  shows \"q \u2228 p\"\nusing 1\nproof (rule disjE)\n  { assume 2: \"p\"\n    show \"q \u2228 p\" using 2 by (rule disjI2) }\nnext\n  { assume 3: \"q\"\n    show \"q \u2228 p\" using 3 by (rule disjI1) }\nqed    \n\n-- \"La demostraci\u00f3n hacia atr\u00e1s con reglas impl\u00edcitas es\"\nlemma ejemplo_12_4:\n  assumes \"p \u2228 q\" \n  shows \"q \u2228 p\"\nusing assms\nproof \n  { assume  \"p\"\n    thus \"q \u2228 p\" .. }\nnext\n  { assume \"q\"\n    thus \"q \u2228 p\" .. }\nqed    \n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_12_5:\n  assumes \"p \u2228 q\" \n  shows \"q \u2228 p\"\nusing assms\nby auto\n\ntext {* \n  Ejemplo 13. (p. 12) Demostrar\n     q \u27f6 r \u22a2 p \u2228 q \u27f6 p \u2228 r\n*}\n\n-- \"La demostraci\u00f3n detallada es\" \nlemma ejemplo_13_1:\n  assumes 1: \"q \u27f6 r\"\n  shows \"p \u2228 q \u27f6 p \u2228 r\"\nproof (rule impI)\n  assume 2: \"p \u2228 q\"\n  thus \"p \u2228 r\"\n  proof (rule disjE)\n    { assume 3: \"p\"\n      show \"p \u2228 r\" using 3 by (rule disjI1) }\n  next\n    { assume 4: \"q\"\n      have 5: \"r\" using 1 4 by (rule mp)\n      show \"p \u2228 r\" using 5 by (rule disjI2) }\n  qed\nqed    \n\n-- \"La demostraci\u00f3n estructurada es\" \nlemma ejemplo_13_2:\n  assumes \"q \u27f6 r\"\n  shows \"p \u2228 q \u27f6 p \u2228 r\"\nproof \n  assume \"p \u2228 q\"\n  thus \"p \u2228 r\"\n  proof \n    { assume \"p\"\n      thus \"p \u2228 r\" .. }\n  next\n    { assume \"q\"\n      have \"r\" using assms `q` ..\n      thus \"p \u2228 r\" .. }\n  qed\nqed    \n\n-- \"La demostraci\u00f3n autom\u00e1tica es\" \nlemma ejemplo_13_3:\n  assumes \"q \u27f6 r\"\n  shows \"p \u2228 q \u27f6 p \u2228 r\"\nusing assms\nby auto\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se ha continuado el estudio de la formalizaci\u00f3n en Isabelle\/HOL de las demostraciones por deducci\u00f3n natural estudiadas en el tema 2 iniciado en la clase anterior. Para cada uno de los ejemplos se ha presentado distintas demostraciones: detallada (que sea parecida a la mostrada&#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":[256],"tags":[144,312,189],"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\/5356"}],"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=5356"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5356\/revisions"}],"predecessor-version":[{"id":5357,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5356\/revisions\/5357"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5356"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5356"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5356"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}