{"id":4215,"date":"2014-03-21T20:18:38","date_gmt":"2014-03-21T19:18:38","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4215"},"modified":"2014-03-26T20:30:44","modified_gmt":"2014-03-26T19:30:44","slug":"lmf2014-ejercicios-de-argumentacion-en-logica-proposicional-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2014-ejercicios-de-argumentacion-en-logica-proposicional-con-isabellehol\/","title":{"rendered":"LMF2014: Ejercicios de argumentaci\u00f3n en l\u00f3gica proposicional con Isabelle\/HOL"},"content":{"rendered":"<p>En la primera parte de la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-13\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha explicado c\u00f3mo formalizar en l\u00f3gica proposicional los argumentos de los ejercicios 3 y 9 de la <a href=\"http:\/\/bit.ly\/1mvmWnu\">relaci\u00f3n 4<\/a> 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  --------------------------------------------------------------------- \r\n  El objetivo de esta es relaci\u00f3n formalizar y demostrar la correcci\u00f3n\r\n  de los argumentos usando s\u00f3lo las reglas b\u00e1sicas de deducci\u00f3n natural\r\n  de la l\u00f3gica proposicional (sin usar el m\u00e9todo auto). \r\n\r\n  Las reglas b\u00e1sicas de la deducci\u00f3n natural son las siguientes:\r\n  \u00b7 conjI:      \u27e6P; Q\u27e7 \u27f9 P \u2227 Q\r\n  \u00b7 conjunct1:  P \u2227 Q \u27f9 P\r\n  \u00b7 conjunct2:  P \u2227 Q \u27f9 Q  \r\n  \u00b7 notnotD:    \u00ac\u00ac P \u27f9 P\r\n  \u00b7 notnotI:    P \u27f9 \u00ac\u00ac P\r\n  \u00b7 mp:         \u27e6P \u27f6 Q; P\u27e7 \u27f9 Q \r\n  \u00b7 mt:         \u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF \r\n  \u00b7 impI:       (P \u27f9 Q) \u27f9 P \u27f6 Q\r\n  \u00b7 disjI1:     P \u27f9 P \u2228 Q\r\n  \u00b7 disjI2:     Q \u27f9 P \u2228 Q\r\n  \u00b7 disjE:      \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R \r\n  \u00b7 FalseE:     False \u27f9 P\r\n  \u00b7 notE:       \u27e6\u00acP; P\u27e7 \u27f9 R\r\n  \u00b7 notI:       (P \u27f9 False) \u27f9 \u00acP\r\n  \u00b7 iffI:       \u27e6P \u27f9 Q; Q \u27f9 P\u27e7 \u27f9 P = Q\r\n  \u00b7 iffD1:      \u27e6Q = P; Q\u27e7 \u27f9 P \r\n  \u00b7 iffD2:      \u27e6P = Q; Q\u27e7 \u27f9 P\r\n  \u00b7 ccontr:     (\u00acP \u27f9 False) \u27f9 P\r\n  --------------------------------------------------------------------- \r\n*}\r\n\r\ntext {*\r\n  Se usar\u00e1n las reglas notnotI y mt que demostramos a continuaci\u00f3n.\r\n  *}\r\n\r\nlemma notnotI: \"P \u27f9 \u00ac\u00ac P\"\r\nby auto\r\n\r\nlemma mt: \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"\r\nby auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 3. Formalizar, y demostrar la correcci\u00f3n, del siguiente\r\n  argumento \r\n     Si no hay control de nacimientos, entonces la poblaci\u00f3n crece\r\n     ilimitadamente; pero si la poblaci\u00f3n crece ilimitadamente,\r\n     aumentar\u00e1 el \u00edndice de pobreza. Por consiguiente, si no hay control\r\n     de nacimientos, aumentar\u00e1 el \u00edndice de pobreza. \r\n  Usar N: Hay control de nacimientos. \r\n       P: La poblaci\u00f3n crece ilimitadamente,\r\n       I: Aumentar\u00e1 el \u00edndice de pobreza. \r\n  ------------------------------------------------------------------ *}\r\n\r\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\r\nlemma ejercicio_3_1:\r\n  \"\u27e6\u00acN \u27f6 P; P \u27f6 I\u27e7 \u27f9 \u00acN \u27f6 I\"\r\nby auto\r\n\r\n-- \"La demostraci\u00f3n estructurada es\"\r\nlemma ejercicio_3_2:\r\n  assumes \"\u00acN \u27f6 P\" \r\n          \"P \u27f6 I\" \r\n  shows   \"\u00acN \u27f6 I\"\r\nproof\r\n  assume \"\u00acN\"\r\n  with assms(1) have \"P\" ..\r\n  with assms(2) show \"I\" ..\r\nqed\r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejercicio_3_3:\r\n  assumes \"\u00acN \u27f6 P\" \r\n          \"P \u27f6 I\" \r\n  shows   \"\u00acN \u27f6 I\"\r\nproof (rule impI)\r\n  assume \"\u00acN\"\r\n  with assms(1) have \"P\" by (rule mp)\r\n  with assms(2) show \"I\" by (rule mp)\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 primera parte de 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 3 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":"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":[234],"tags":[144,303,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\/4215"}],"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=4215"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4215\/revisions"}],"predecessor-version":[{"id":4217,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4215\/revisions\/4217"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4215"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4215"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4215"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}