{"id":3173,"date":"2013-04-03T14:12:17","date_gmt":"2013-04-03T14:12:17","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3173"},"modified":"2013-04-04T06:44:53","modified_gmt":"2013-04-04T06:44:53","slug":"lmf2013-ejercicios-de-argumentacion-en-logica-proposicional-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-ejercicios-de-argumentacion-en-logica-proposicional-con-isabellehol\/","title":{"rendered":"LMF2013: Ejercicios de argumentaci\u00f3n en l\u00f3gica proposicional con Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-12\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha explicado c\u00f3mo formalizar en l\u00f3gica proposicional los argumentos de los ejercicios 8 y 9 de la relaci\u00f3n 4 y c\u00f3mo demostrar con Isabelle\/HOL su correcci\u00f3n.<\/p>\n<p>Los ejercicios y sus soluciones se muestran a continuaci\u00f3n:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 8. Formalizar, y demostrar la correcci\u00f3n, del siguiente\r\n  argumento \r\n     Si el general era leal, hubiera obedecido las \u00f3rdenes, y si era\r\n     inteligente las hubiera comprendido. O el general desobedeci\u00f3 las\r\n     \u00f3rdenes o no las comprendi\u00f3. Luego, el general era desleal o no era\r\n     inteligente. \r\n  Usar L:  El general es leal.\r\n       Ob: El general obedece las \u00f3rdenes.\r\n       I:  El general es inteligente.\r\n       C:  El general comprende las \u00f3rdenes.\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_8_1:\r\n  assumes \"(L \u27f6 Ob) \u2227 (I \u27f6 C)\" \r\n          \"\u00acOb \u2228 \u00acC\" \r\n  shows   \"\u00acL \u2228 \u00acI\"\r\nusing assms\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_8_2:\r\n  assumes \"(L \u27f6 Ob) \u2227 (I \u27f6 C)\" \r\n          \"\u00acOb \u2228 \u00acC\" \r\n  shows   \"\u00acL \u2228 \u00acI\"\r\nusing assms(2)\r\nproof\r\n  assume \"\u00acOb\"\r\n  have \"L \u27f6 Ob\" using assms(1) ..\r\n  hence \"\u00acL\" using `\u00acOb` by (rule mt)\r\n  thus \"\u00acL \u2228 \u00acI\" ..\r\nnext\r\n  assume \"\u00acC\"\r\n  have \"I \u27f6 C\" using assms(1) ..\r\n  hence \"\u00acI\" using `\u00acC` by (rule mt)\r\n  thus \"\u00acL \u2228 \u00acI\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_8_3:\r\n  assumes \"(L \u27f6 Ob) \u2227 (I \u27f6 C)\" \r\n          \"\u00acOb \u2228 \u00acC\" \r\n  shows   \"\u00acL \u2228 \u00acI\"\r\nusing assms(2)\r\nproof (rule disjE)\r\n  assume \"\u00acOb\"\r\n  have \"L \u27f6 Ob\" using assms(1) by (rule conjunct1)\r\n  hence \"\u00acL\" using `\u00acOb` by (rule mt)\r\n  thus \"\u00acL \u2228 \u00acI\" by (rule disjI1)\r\nnext\r\n  assume \"\u00acC\"\r\n  have \"I \u27f6 C\" using assms(1) by (rule conjunct2)\r\n  hence \"\u00acI\" using `\u00acC` by (rule mt)\r\n  thus \"\u00acL \u2228 \u00acI\" by (rule disjI2)\r\nqed\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 9. Formalizar, y demostrar la correcci\u00f3n, del siguiente\r\n  argumento \r\n     Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo\r\n     har\u00eda. Si Dios fuera incapaz de evitar el mal, no ser\u00eda\r\n     omnipotente; si no quisiera evitar el mal ser\u00eda mal\u00e9volo. Dios no\r\n     evita el mal. Si Dios existe, es omnipotente y no es\r\n     mal\u00e9volo. Luego, Dios no existe. \r\n  Usar C:  Dios es capaz de evitar el mal.\r\n       Q:  Dios quiere evitar el mal.\r\n       Om: Dios es omnipotente.\r\n       M:  Dios es mal\u00e9volo.\r\n       P:  Dios evita el mal.\r\n       E:  Dios existe.\r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_9_1:\r\n  assumes \"C \u2227 Q \u27f6 P\" \r\n          \"(\u00acC \u27f6 \u00acOm) \u2227 (\u00acQ \u27f6 M)\" \r\n          \"\u00acP\" \r\n          \"E \u27f6 Om \u2227 \u00acM\" \r\n  shows   \"\u00acE\"\r\nusing assms\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_9_2:\r\n  assumes \"C \u2227 Q \u27f6 P\" \r\n          \"(\u00acC \u27f6 \u00acOm) \u2227 (\u00acQ \u27f6 M)\" \r\n          \"\u00acP\" \r\n          \"E \u27f6 Om \u2227 \u00acM\" \r\n  shows   \"\u00acE\"\r\nproof\r\n  assume \"E\"\r\n  have \"Om \u2227 \u00acM\" using assms(4) `E` ..\r\n  hence \"Om\" ..\r\n  hence \"\u00ac\u00acOm\" by (rule notnotI)\r\n  have \"\u00acC \u27f6 \u00acOm\" using assms(2) ..\r\n  hence \"\u00ac\u00acC\" using `\u00ac\u00acOm` by (rule mt)\r\n  hence \"C\" by (rule notnotD)\r\n  have \"\u00acM\" using `Om \u2227 \u00acM` ..\r\n  have \"\u00acQ \u27f6 M\" using assms(2) ..\r\n  hence \"\u00ac\u00acQ\" using `\u00acM` by (rule mt)\r\n  hence \"Q\" by (rule notnotD)\r\n  with `C` have \"C \u2227 Q\" ..\r\n  with assms(1) have \"P\" ..\r\n  with assms(3) show False ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_9_3:\r\n  assumes \"C \u2227 Q \u27f6 P\" \r\n          \"(\u00acC \u27f6 \u00acOm) \u2227 (\u00acQ \u27f6 M)\" \r\n          \"\u00acP\" \r\n          \"E \u27f6 Om \u2227 \u00acM\" \r\n  shows   \"\u00acE\"\r\nproof (rule notI)\r\n  assume \"E\"\r\n  with assms(4) have \"Om \u2227 \u00acM\" by (rule mp)\r\n  hence \"Om\" by (rule conjunct1)\r\n  hence \"\u00ac\u00acOm\" by (rule notnotI)\r\n  have \"\u00acC \u27f6 \u00acOm\" using assms(2) by (rule conjunct1)\r\n  hence \"\u00ac\u00acC\" using `\u00ac\u00acOm` by (rule mt)\r\n  hence \"C\" by (rule notnotD)\r\n  have \"\u00acM\" using `Om \u2227 \u00acM` by (rule conjunct2)\r\n  have \"\u00acQ \u27f6 M\" using assms(2) by (rule conjunct2)\r\n  hence \"\u00ac\u00acQ\" using `\u00acM` by (rule mt)\r\n  hence \"Q\" by (rule notnotD)\r\n  with `C` have \"C \u2227 Q\" by (rule conjI)\r\n  with assms(1) have \"P\" by (rule mp)\r\n  with assms(3) show False by (rule notE)\r\nqed\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se ha explicado c\u00f3mo formalizar en l\u00f3gica proposicional los argumentos de los ejercicios 8 y 9 de la relaci\u00f3n 4 y c\u00f3mo demostrar con Isabelle\/HOL su correcci\u00f3n. Los ejercicios y sus soluciones se muestran a continuaci\u00f3n:<\/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":[1],"tags":[206,84,144,202,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\/3173"}],"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=3173"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3173\/revisions"}],"predecessor-version":[{"id":3176,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3173\/revisions\/3176"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3173"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3173"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3173"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}