{"id":235,"date":"2020-03-31T11:29:06","date_gmt":"2020-03-31T09:29:06","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=235"},"modified":"2021-08-21T13:20:13","modified_gmt":"2021-08-21T11:20:13","slug":"el-problema-del-barbero","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/el-problema-del-barbero\/","title":{"rendered":"El problema del barbero"},"content":{"rendered":"<p>Decidir si es cierto que<\/p>\n<blockquote><p>\nCarlos afeita a todos los habitantes de Las Chinas que no se afeitan a s\u00ed mismo y s\u00f3lo a ellos. Carlos es un habitante de las Chinas. Por consiguiente, Carlos no afeita a nadie.\n<\/p><\/blockquote>\n<p>Se usar\u00e1 la siguiente simbolizaci\u00f3n:<\/p>\n<ul>\n<li>A(x,y) para x afeita a y<\/li>\n<li>C(x)   para x es un habitante de Las Chinas<\/li>\n<li>c      para Carlos<\/li>\n<\/ul>\n<p>El problema consiste en completar la siguiente teor\u00eda de Isabelle\/HOL:<\/p>\n<pre lang=\"isar\">\ntheory El_problema_del_barbero\nimports Main\nbegin\n\nlemma\n  assumes \"\u2200x. A(c,x) \u27f7 C(x) \u2227 \u00acA(x,x)\"\n          \"C(c)\"\n  shows   \"\u00ac(\u2203x. A(c,x))\"\n  oops\nend\n<\/pre>\n<h4>Soluciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory El_problema_del_barbero\nimports Main\nbegin\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma\n  assumes \"\u2200x. A(c,x) \u27f7 C(x) \u2227 \u00acA(x,x)\"\n          \"C(c)\"\n  shows   \"\u00ac(\u2203x. A(c,x))\"\n  using assms\n  by auto\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma\n  assumes \"\u2200x. A(c,x) \u27f7 C(x) \u2227 \u00acA(x,x)\"\n          \"C(c)\"\n  shows   \"\u00ac(\u2203x. A(c,x))\"\nproof -\n  have 1: \"A(c,c) \u27f7 C(c) \u2227 \u00acA(c,c)\" using assms(1) ..\n  have \"A(c,c)\"\n  proof (rule ccontr)\n    assume \"\u00acA(c,c)\"\n    with assms(2) have \"C(c) \u2227 \u00acA(c,c)\" ..\n    with 1 have \"A(c,c)\" ..\n    with \u2039\u00acA(c,c)\u203a show False ..\n  qed\n  have \"\u00acA(c,c)\"\n  proof -\n    have \"C(c) \u2227 \u00acA(c,c)\" using 1 \u2039A(c,c)\u203a ..\n    then show \"\u00acA(c,c)\" ..\n  qed\n  then show \"\u00ac(\u2203x. A(c,x))\" using \u2039A(c,c)\u203a ..\nqed\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma\n  assumes \"\u2200x. A(c,x) \u27f7 C(x) \u2227 \u00acA(x,x)\"\n          \"C(c)\"\n  shows   \"\u00ac(\u2203x. A(c,x))\"\nproof -\n  have 1: \"A(c,c) \u27f7 C(c) \u2227 \u00acA(c,c)\" using assms(1) by (rule allE)\n  have \"A(c,c)\"\n  proof (rule ccontr)\n    assume \"\u00acA(c,c)\"\n    with assms(2) have \"C(c) \u2227 \u00acA(c,c)\" by (rule conjI)\n    with 1 have \"A(c,c)\" by (rule iffD2)\n    with \u2039\u00acA(c,c)\u203a show False by (rule notE)\n  qed\n  have \"\u00acA(c,c)\"\n  proof -\n    have \"C(c) \u2227 \u00acA(c,c)\" using 1 \u2039A(c,c)\u203a by (rule iffD1)\n    then show \"\u00acA(c,c)\" by (rule conjunct2)\n  qed\n  then show \"\u00ac(\u2203x. A(c,x))\" using \u2039A(c,c)\u203a by (rule notE)\nqed\n\nend\n<\/pre>\n<h4>Otras soluciones<\/h4>\n<ul>\n<li>Se pueden escribir otras soluciones en los comentarios.\n<li>El c\u00f3digo se debe escribir entre una l\u00ednea con &#60;pre lang=&quot;isar&quot;&#62; y otra con &#60;\/pre&#62;\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Decidir si es cierto que Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a s\u00ed mismo y s\u00f3lo a ellos. Carlos es un habitante de las Chinas. Por consiguiente, Carlos no afeita a nadie. Se usar\u00e1 la siguiente simbolizaci\u00f3n: A(x,y) para x afeita a y C(x) para x es un habitante de Las Chinas c para Carlos El problema consiste en completar la siguiente teor\u00eda de Isabelle\/HOL: theory El_problema_del_barbero imports Main begin lemma assumes \u00ab\u2200x. A(c,x) \u27f7 C(x) \u2227 \u00acA(x,x)\u00bb \u00abC(c)\u00bb shows \u00ab\u00ac(\u2203x. A(c,x))\u00bb oops end Soluciones con Isabelle\/HOL theory El_problema_del_barbero imports Main begin \u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a lemma assumes \u00ab\u2200x. A(c,x) \u27f7 C(x) \u2227 \u00acA(x,x)\u00bb \u00abC(c)\u00bb shows \u00ab\u00ac(\u2203x. A(c,x))\u00bb using assms by auto \u2015 \u2039La demostraci\u00f3n estructurada es\u203a&#8230;<\/p>\n","protected":false},"author":1,"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,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[103],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/235"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=235"}],"version-history":[{"count":5,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/235\/revisions"}],"predecessor-version":[{"id":267,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/235\/revisions\/267"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=235"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=235"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=235"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}