{"id":3750,"date":"2013-10-09T17:39:26","date_gmt":"2013-10-09T15:39:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3750"},"modified":"2013-10-09T17:39:26","modified_gmt":"2013-10-09T15:39:26","slug":"li2013-ejercicios-de-logica-proposicional-4","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/li2013-ejercicios-de-logica-proposicional-4\/","title":{"rendered":"LI2013: Ejercicios de l\u00f3gica proposicional (4)"},"content":{"rendered":"<p>En la segunda parte de la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-13\">L\u00f3gica Inform\u00e1tica<\/a> se han comentado las soluciones de los ejercicios de la 4\u00aa relaci\u00f3n.<\/p>\n<p>Los ejercicios, y sus soluciones con <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/\">Isabelle\/HOL<\/a>, se muestran a continuaci\u00f3n:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* R4: Representaci\u00f3n del conocimiento proposicional (4) *}\r\n\r\ntheory R4\r\nimports Main \r\nbegin\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 1. Formalizar, y decidir 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\nlemma \r\n  assumes \"(L \u27f6 Ob) \u2227 (I \u27f6 C)\" \r\n          \"\u00acOb \u2228 \u00acC\" \r\n  shows   \"\u00acL \u2228 \u00acI\"\r\nusing assms by auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 2. Un rey somete a un prisionero a la siguiente prueba: lo\r\n  enfrenta a dos puertas, de las que el prisionero debe elegir una, y\r\n  entrar en la habitaci\u00f3n correspondiente. Se informa al prisionero que\r\n  en cada una de las habitaciones puede haber un tigre o una dama. Como\r\n  es natural, el prisionero debe elegir la puerta que le lleva a la dama\r\n  (entre otras cosas, para no ser devorado por el tigre). Para ayudarle,\r\n  en cada puerta hay un letrero: \r\n  \u00b7 puerta 1: en esta habitaci\u00f3n hay una dama y en la otra un tigre.\r\n  \u00b7 puerta 2: en una de estas habitaciones hay una dama y en una de estas\r\n              habitaciones hay un tigre.\r\n  Sabiendo que uno de los carteles dice la verdad y el otro no,\r\n  determinar la puerta que debe de elegir el prisionero.  \r\n  ------------------------------------------------------------------ *}\r\n\r\ntext {*\r\n  Soluci\u00f3n: Para la representaci\u00f3n usaremos los siguientes s\u00edmbolos, con\r\n  el significado indicado,\r\n    \u00b7 p1 que representa \"el cartel de la puerta 1 es verdadero\", \r\n    \u00b7 p2 que representa \"el cartel de la puerta 2 es verdadero\", \r\n    \u00b7 d1 que representa \"hay una dama en la habitaci\u00f3n 1\",\r\n    \u00b7 d2 que representa \"hay una dama en la habitaci\u00f3n 2\",\r\n    \u00b7 t1 que representa \"hay un tigre en la habitaci\u00f3n 1\",\r\n    \u00b7 t2 que representa \"hay un tigre en la habitaci\u00f3n 2\",\r\n\r\n  En primer lugar representamos el problema y buscamos modelos de las hip\u00f3tesis:\r\n*}\r\n\r\nlemma \r\n  assumes \"(d1 \u2228 t1) \u2227 (d2 \u2228 t2)\"\r\n          \"p1 \u27f7 d1 \u2227 t2\"\r\n          \"p2 \u27f7 (d1 \u2228 d2) \u2227 (t1 \u2228 t2)\"\r\n          \"(p1 \u2227 \u00acp2) \u2228 (\u00acp1 \u2227 p2)\"\r\n  shows   False\r\nquickcheck\r\noops\r\n\r\ntext {*\r\n  Quickcheck encuentra el siguiente modelo:\r\n    d1 = False\r\n    t1 = True\r\n    d2 = True\r\n    t2 = False\r\n    p1 = False\r\n    p2 = True\r\n\r\n  Se observa que, en el modelo, la dama est\u00e1 en la 2\u00aa habitaci\u00f3n. Para\r\n  demostrar que efectivamente esa es la respuesta, lo demostramos con auto:\r\n*}\r\n\r\nlemma \r\n  assumes \"(d1 \u2228 t1) \u2227 (d2 \u2228 t2)\"\r\n          \"p1 \u27f7 d1 \u2227 t2\"\r\n          \"p2 \u27f7 (d1 \u2228 d2) \u2227 (t1 \u2228 t2)\"\r\n          \"(p1 \u2227 \u00acp2) \u2228 (\u00acp1 \u2227 p2)\"\r\n  shows   \"d2\"\r\nusing assms by auto\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 3. Decidir razonadamente si las siguientes afirmaciones son\r\n  correctas: \r\n  1. Si S \u22a8 F, entonces S \u222a {F} es consistente.\r\n  2. Si S \u22a8 F, entonces S \u222a {F} es inconsistente.\r\n  ------------------------------------------------------------------ *}\r\n\r\ntext {*\r\n  Soluci\u00f3n del apartado 1: La afirmaci\u00f3n es falsa. Por ejemplo,\r\n  eligiendo como S el conjunto {p \u2227 \u00acp} y como F la f\u00f3rmula q, se\r\n  tiene que \r\n  \u00b7 S \u22a8 F (ya que p \u2227 \u00acp no tiene modelos) y \r\n  \u00b7 S \u222a {F} es inconsistente (por la misma raz\u00f3n). \r\n\r\n  Soluci\u00f3n del apartado 2: La afirmaci\u00f3n es falsa. Por ejemplo,\r\n  eligiendo como S el conjunto {p \u2227 q} y como F la f\u00f3rmula q, se\r\n  tiene que \r\n  \u00b7 S \u22a8 F (ya que si I es modelo de S, entonces I(p \u2227 q) = 1 y, por\r\n    tanto, I(q) = 1) y \r\n  \u00b7 S \u222a {F} es consistente (un modelo es la interpretaci\u00f3n I con \r\n    I(p) = I(q) = 1.\r\n*}\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la segunda parte de la clase de hoy del curso L\u00f3gica Inform\u00e1tica se han comentado las soluciones de los ejercicios de la 4\u00aa relaci\u00f3n. Los ejercicios, y sus soluciones con Isabelle\/HOL, 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":[223],"tags":[144,301,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\/3750"}],"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=3750"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3750\/revisions"}],"predecessor-version":[{"id":3751,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3750\/revisions\/3751"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3750"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3750"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3750"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}