{"id":4220,"date":"2014-03-21T20:35:18","date_gmt":"2014-03-21T19:35:18","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4220"},"modified":"2014-03-26T20:36:41","modified_gmt":"2014-03-26T19:36:41","slug":"lmf2014-ejercicios-de-formalizacion-en-logica-de-primer-orden-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2014-ejercicios-de-formalizacion-en-logica-de-primer-orden-con-isabellehol\/","title":{"rendered":"LMF2014: Ejercicios de formalizaci\u00f3n en l\u00f3gica de primer orden con Isabelle\/HOL"},"content":{"rendered":"

En la segunda parte de la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha explicado c\u00f3mo formalizar en l\u00f3gica de primer orden los argumentos de los ejercicios 8, 12 y 26 de la relaci\u00f3n 5<\/a>.<\/p>\n

Los ejercicios y sus soluciones se muestran a continuaci\u00f3n:
\n<\/p>\n

\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 8. Formalizar el siguiente argumento \r\n     Quien intente entrar en un pa\u00eds y no tenga pasaporte, encontrar\u00e1\r\n     alg\u00fan aduanero que le impida el paso. A algunas personas\r\n     motorizadas que intentan entrar en un pa\u00eds le impiden el paso\r\n     \u00fanicamente personas motorizadas. Ninguna persona motorizada tiene\r\n     pasaporte. Por tanto, ciertos aduaneros est\u00e1n motorizados.\r\n  Usar E(x)   para x entra en un pa\u00eds\r\n       P(x)   para x tiene pasaporte\r\n       A(x)   para x es aduanero\r\n       I(x,y) para x impide el paso a y\r\n       M(x)   para x est\u00e1 motorizada\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_8:\r\n  assumes \"\u2200x. E(x) \u2227 \u00acP(x) \u27f6 (\u2203y. A(y) \u2227 I(y,x))\"\r\n          \"\u2203x. M(x) \u2227 E(x) \u2227 (\u2200y. I(y,x) \u27f6 M(y))\"\r\n          \"\u2200x. M(x) \u27f6 \u00acP(x)\"\r\n  shows \"\u2203x. A(x) \u2227 M(x)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 12. Formalizar el siguiente argumento \r\n     Toda persona pobre tiene un padre rico. Por tanto, existe una\r\n     persona rica que tiene un abuelo rico.\r\n  Usar R(x) para x es rico\r\n       p(x) para el padre de x\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_12:\r\n  assumes \"\u2200x. \u00acR(x) \u27f6 R(p(x))\"\r\n  shows   \"\u2203x. R(x) \u2227 R(p(p(x)))\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 26. Formalizar el siguiente argumento \r\n     S\u00f3lo hay un sofista que ense\u00f1a gratuitamente, y \u00e9ste es\r\n     S\u00f3crates. S\u00f3crates argumenta mejor que ning\u00fan otro sofista. Plat\u00f3n\r\n     argumenta mejor que alg\u00fan sofista que ense\u00f1a gratuitamente. Si una\r\n     persona argumenta mejor que otra segunda, entonces la segunda no\r\n     argumenta mejor que la primera. Por consiguiente, Plat\u00f3n no es un\r\n     sofista. \r\n  Usar G(x)   para x ense\u00f1a gratuitamente\r\n       M(x,y) para x argumenta mejor que y\r\n       S(x)   para x es un sofista\r\n       p      para Plat\u00f3n\r\n       s      para S\u00f3crates\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_26:\r\n  assumes \"\u2203y. (\u2200x. S(x) \u2227 G(x) \u27f7 x=y) \u2227 y=s\" \r\n          \"\u2200x. S(x) \u2227 x \u2260 s \u27f6 M(s,x)\" \r\n          \"\u2203x. S(x) \u2227 G(x) \u2227 M(p,x)\"  \r\n          \"\u2200x y. M(x,y) \u27f6 \u00acM(y,x)\"\r\n  shows \"\u00acS(p)\"\r\noops\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"
En la segunda parte de la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se ha explicado c\u00f3mo formalizar en l\u00f3gica de primer orden los argumentos de los ejercicios 8, 12 y 26 de la relaci\u00f3n 5. 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":[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\/4220"}],"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=4220"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4220\/revisions"}],"predecessor-version":[{"id":4221,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4220\/revisions\/4221"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4220"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4220"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4220"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}