{"id":5718,"date":"2017-02-21T18:06:18","date_gmt":"2017-02-21T17:06:18","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5718"},"modified":"2017-02-23T18:07:18","modified_gmt":"2017-02-23T17:07:18","slug":"lmf2017-deduccion-natural-proposicional-2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2017-deduccion-natural-proposicional-2\/","title":{"rendered":"LMF2017: Deducci\u00f3n natural proposicional (2)"},"content":{"rendered":"<p>En la segunda parte de la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-16\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha continuado el estudio de la deducci\u00f3n natural en la l\u00f3gica proposicional.<\/p>\n<p>Se han estudiado las siguientes reglas b\u00e1sicas<\/p>\n<ul>\n<li>Regla de copia<\/li>\n<li>Reglas de la negaci\u00f3n<\/li>\n<li>Reglas del bicondicional<\/li>\n<\/ul>\n<p>y la siguientes reglas derivadas:<\/p>\n<ul>\n<li>Regla del modus tollens<\/li>\n<li>Regla de introducci\u00f3n de doble negaci\u00f3n<\/li>\n<li>Regla de reducci\u00f3n al absurdo<\/li>\n<li>Ley del tercio excluido<\/li>\n<\/ul>\n<p>Finalmente, se ha comentado la instalaci\u00f3n de <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/\">Isabelle<\/a> y su uso para demostrar una f\u00f3rmula con distinto nivel de detalle.<\/p>\n<p>Las transparencias de esta clase son las 12-29 del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-16\/temas\/tema-2.pdf\">tema 2<\/a> y la teor\u00eda Isabelle es<br \/>\n<!-- more --><\/p>\n<pre lang=\"isar\">\nheader {* Tema 2: Deducci\u00f3n natural proposicional con Isabelle\/HOL *}\n \ntheory T2\nimports Main \nbegin\n \ntext {*\n  En este tema se presentan los ejemplos del tema de deducci\u00f3n natural\n  proposicional siguiendo la presentaci\u00f3n de Huth y Ryan en su libro\n  \"Logic in Computer Science\" http:\/\/goo.gl\/qsVpY y, m\u00e1s concretamente,\n  a la forma como se explica en la asignatura.\n \n  La p\u00e1gina al lado de cada ejemplo indica la p\u00e1gina de las transparencias \n  donde se encuentra la demostraci\u00f3n. *}\n \nsubsection {* Reglas de la conjunci\u00f3n *}\n \ntext {* \n  Ejemplo 1 (p. 4). Demostrar que\n     p \u2227 q, r \u22a2 q \u2227 r.\n  *}     \n \n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_1_1:\n  assumes 1: \"p \u2227 q\" and\n          2: \"r\" \n  shows \"q \u2227 r\"     \nproof -\n  have 3: \"q\" using 1 by (rule conjunct2)\n  show 4: \"q \u2227 r\" using 3 2 by (rule conjI)\nqed\nthm ejemplo_1_1\ntext {*\n  Notas sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"assumes\" para indicar las hip\u00f3tesis,\n  \u00b7 \"and\" para separar las hip\u00f3tesis,\n  \u00b7 \"shows\" para indicar la conclusi\u00f3n,\n  \u00b7 \"proof\" para iniciar la prueba,\n  \u00b7 \"qed\" para terminar la pruebas,\n  \u00b7 \"-\" (despu\u00e9s de \"proof\") para no usar el m\u00e9todo por defecto,\n  \u00b7 \"have\" para establecer un paso,\n  \u00b7 \"using\" para usar hechos en un paso,\n  \u00b7 \"by (rule ..)\" para indicar la regla con la que se peueba un hecho,\n  \u00b7 \"show\" para establecer la conclusi\u00f3n.\n \n  Notas sobre la l\u00f3gica: Las reglas de la conjunci\u00f3n son\n  \u00b7 conjI:      \u27e6P; Q\u27e7 \u27f9 P \u2227 Q\n  \u00b7 conjunct1:  P \u2227 Q \u27f9 P\n  \u00b7 conjunct2:  P \u2227 Q \u27f9 Q  \n*}\n \ntext {* Se pueden dejar impl\u00edcitas las reglas como sigue *}\n \nlemma ejemplo_1_2:\n  assumes 1: \"p \u2227 q\" and \n          2: \"r\" \n  shows \"q \u2227 r\"     \nproof -\n  have 3: \"q\" using 1 .. \n  show 4: \"q \u2227 r\" using 3 2 ..\nqed\n \ntext {*\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"..\" para indicar que se prueba por la regla correspondiente. *}\n \ntext {* Se pueden eliminar las etiquetas como sigue *}\n \nlemma ejemplo_1_3:\n  assumes \"p \u2227 q\" \n          \"r\" \n  shows   \"q \u2227 r\"     \nproof -\n  have \"q\" using assms(1) ..\n  thus \"q \u2227 r\" using assms(2) ..\nqed\n \ntext {*\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"assms(n)\" para indicar la hip\u00f3tesis n y\n  \u00b7 \"thus\" para demostrar la conclusi\u00f3n usando el hecho anterior.\n  Adem\u00e1s, no es necesario usar and entre las hip\u00f3tesis. *}\n \ntext {* Se puede automatizar la demostraci\u00f3n como sigue *}\n \nlemma ejemplo_1_4:\n  assumes \"p \u2227 q\" \n          \"r\" \n  shows   \"q \u2227 r\"     \nusing assms\nby auto\n \ntext {*\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"assms\" para indicar las hip\u00f3tesis y\n  \u00b7 \"by auto\" para demostrar la conclusi\u00f3n autom\u00e1ticamente. *}\n \ntext {* Se puede automatizar totalmente la demostraci\u00f3n como sigue *}\n \nlemma ejemplo_1_5:\n  \"\u27e6p \u2227 q; r\u27e7 \u27f9 q \u2227 r\"\nby auto\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la segunda parte de la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se ha continuado el estudio de la deducci\u00f3n natural en la l\u00f3gica proposicional. Se han estudiado las siguientes reglas b\u00e1sicas Regla de copia Reglas de la negaci\u00f3n Reglas del bicondicional y la siguientes reglas derivadas: Regla del modus tollens Regla&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","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":[264],"tags":[144,315,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\/5718"}],"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=5718"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5718\/revisions"}],"predecessor-version":[{"id":5719,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5718\/revisions\/5719"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5718"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5718"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5718"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}