{"id":2555,"date":"2013-03-07T18:30:26","date_gmt":"2013-03-07T18:30:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2555"},"modified":"2013-03-08T05:47:33","modified_gmt":"2013-03-08T05:47:33","slug":"ra2012-introduccion-a-la-demostracion-asistida-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2012-introduccion-a-la-demostracion-asistida-con-isabellehol\/","title":{"rendered":"RA2012: Introducci\u00f3n a la demostraci\u00f3n asistida con Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\">Razonamiento autom\u00e1tico<\/a> se ha presentado:<\/p>\n<ul>\n<li>una <a href=\"http:\/\/goo.gl\/NWk7b\">visi\u00f3n panor\u00e1mica del razonamiento asistido por computador<\/a>,\n<li>un panorama del <a href=\"http:\/\/goo.gl\/il9T8\">contenido de la asignatura<\/a>:\n<ul>\n<li>deducci\u00f3n natural en Isabelle\/HOL,\n<li>programaci\u00f3n funcional en Isabelle\/HOL,\n<li>razonamiento sobre programas.\n<\/ul>\n<li>un ejemplo de demostraci\u00f3n por deducci\u00f3n natural en Isabelle\/HOL\n<li>una visi\u00f3n general de las <a href=\"http:\/\/goo.gl\/KMcuc\">teor\u00edas de HOL<\/a>.\n<\/ul>\n<p>El ejemplo que se ha visto para introducir los elementos del lenguaje de demostraci\u00f3n es el siguiente<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* Tema 3: Deducci\u00f3n natural proposicional con Isabelle\/HOL *}\r\n\r\ntheory T3\r\nimports Main \r\nbegin\r\n\r\ntext {*\r\n  En esta secci\u00f3n se presentan los ejemplos del tema de deducci\u00f3n natural\r\n  proposicional siguiendo la presentaci\u00f3n de Huth y Ryan en su libro\r\n  \"Logic in Computer Science\" http:\/\/goo.gl\/qsVpY y, m\u00e1s concretamente,\r\n  a la forma como se explica en la asignatura de \"L\u00f3gica inform\u00e1tica\" (LI) \r\n  http:\/\/goo.gl\/AwDiv\r\n \r\n  La p\u00e1gina al lado de cada ejemplo indica la p\u00e1gina de las transparencias \r\n  de LI donde se encuentra la demostraci\u00f3n. *}\r\n\r\nsubsection {* Reglas de la conjunci\u00f3n *}\r\n\r\ntext {* \r\n  Ejemplo 1 (p. 4). Demostrar que\r\n     p \u2227 q, r \u22a2 q \u2227 r.\r\n  *}     \r\n\r\n-- \"La demostraci\u00f3n detallada es\"\r\nlemma ejemplo_1_1:\r\n  assumes 1: \"p \u2227 q\" and\r\n          2: \"r\" \r\n  shows \"q \u2227 r\"     \r\nproof -\r\n  have 3: \"q\" using 1 by (rule conjunct2)\r\n  show 4: \"q \u2227 r\" using 3 2 by (rule conjI)\r\nqed\r\n\r\ntext {*\r\n  Notas sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\r\n  \u00b7 \"assumes\" para indicar las hip\u00f3tesis,\r\n  \u00b7 \"and\" para separar las hip\u00f3tesis,\r\n  \u00b7 \"shows\" para indicar la conclusi\u00f3n,\r\n  \u00b7 \"proof\" para iniciar la prueba,\r\n  \u00b7 \"qed\" para terminar la pruebas,\r\n  \u00b7 \"-\" (despu\u00e9s de \"proof\") para no usar el m\u00e9todo por defecto,\r\n  \u00b7 \"have\" para establecer un paso,\r\n  \u00b7 \"using\" para usar hechos en un paso,\r\n  \u00b7 \"by (rule ..)\" para indicar la regla con la que se peueba un hecho,\r\n  \u00b7 \"show\" para establecer la conclusi\u00f3n.\r\n\r\n  Notas sobre la l\u00f3gica: Las reglas de la conjunci\u00f3n son\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*}\r\n\r\ntext {* Se pueden dejar impl\u00edcitas las reglas como sigue *}\r\n\r\nlemma ejemplo_1_2:\r\n  assumes 1: \"p \u2227 q\" and \r\n          2: \"r\" \r\n  shows \"q \u2227 r\"     \r\nproof -\r\n  have 3: \"q\" using 1 .. \r\n  show 4: \"q \u2227 r\" using 3 2 ..\r\nqed\r\n\r\ntext {*\r\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\r\n  \u00b7 \"..\" para indicar que se prueba por la regla correspondiente. *}\r\n\r\ntext {* Se pueden eliminar las etiquetas como sigue *}\r\n\r\nlemma ejemplo_1_3:\r\n  assumes \"p \u2227 q\" \r\n          \"r\" \r\n  shows   \"q \u2227 r\"     \r\nproof -\r\n  have \"q\" using assms(1) ..\r\n  thus \"q \u2227 r\" using assms(2) ..\r\nqed\r\n\r\ntext {*\r\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\r\n  \u00b7 \"assms(n)\" para indicar la hip\u00f3tesis n y\r\n  \u00b7 \"thus\" para demostrar la conclusi\u00f3n usando el hecho anterior.\r\n  Adem\u00e1s, no es necesario usar and entre las hip\u00f3tesis. *}\r\n\r\ntext {* Se puede automatizar la demostraci\u00f3n como sigue *}\r\n  \r\nlemma ejemplo_1_4:\r\n  assumes \"p \u2227 q\" \r\n          \"r\" \r\n  shows   \"q \u2227 r\"     \r\nusing assms\r\nby auto\r\n\r\ntext {*\r\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\r\n  \u00b7 \"assms\" para indicar las hip\u00f3tesis y\r\n  \u00b7 \"by auto\" para demostrar la conclusi\u00f3n autom\u00e1ticamente. *}\r\n\r\ntext {* Se puede automatizar totalmente la demostraci\u00f3n como sigue *}\r\n\r\nlemma ejemplo_1_5:\r\n  \"\u27e6p \u2227 q; r\u27e7 \u27f9 q \u2227 r\"\r\nby auto\r\n\r\ntext {*\r\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\r\n  \u00b7 \"\u27e6 ... \u27e7\" para representar las hip\u00f3tesis,\r\n  \u00b7 \";\" para separar las hip\u00f3tesis y\r\n  \u00b7 \"\u27f9\" para separar las hip\u00f3tesis de la conclusi\u00f3n. *}\r\n\r\ntext {* Se puede hacer la demostraci\u00f3n por razonamiento hacia atr\u00e1s,\r\n  como sigue *}\r\n\r\nlemma ejemplo_1_6:\r\n  assumes \"p \u2227 q\" \r\n      and \"r\" \r\n  shows   \"q \u2227 r\"     \r\nproof (rule conjI)\r\n  show \"q\" using assms(1) by (rule conjunct2)\r\nnext\r\n  show \"r\" using assms(2) by this\r\nqed\r\n\r\ntext {*\r\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\r\n  \u00b7 \"proof (rule r)\" para indicar que se har\u00e1 la demostraci\u00f3n con la\r\n    regla r,\r\n  \u00b7 \"next\" para indicar el comienzo de la prueba del siguiente\r\n    subobjetivo,\r\n  \u00b7 \"this\" para indicar el hecho actual. *}\r\n\r\ntext {* Se pueden dejar impl\u00edcitas las reglas como sigue *}\r\n\r\nlemma ejemplo_1_7:\r\n  assumes \"p \u2227 q\" \r\n          \"r\" \r\n  shows   \"q \u2227 r\"     \r\nproof \r\n  show \"q\" using assms(1) ..\r\nnext\r\n  show \"r\" using assms(2) . \r\nqed\r\n\r\ntext {*\r\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\r\n  \u00b7 \".\" para indicar por el hecho actual. *}\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se ha presentado: una visi\u00f3n panor\u00e1mica del razonamiento asistido por computador, un panorama del contenido de la asignatura: deducci\u00f3n natural en Isabelle\/HOL, programaci\u00f3n funcional en Isabelle\/HOL, razonamiento sobre programas. un ejemplo de demostraci\u00f3n por deducci\u00f3n natural en Isabelle\/HOL una visi\u00f3n general de las teor\u00edas de&#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":[1],"tags":[144,203],"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\/2555"}],"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=2555"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2555\/revisions"}],"predecessor-version":[{"id":2677,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2555\/revisions\/2677"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2555"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2555"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2555"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}