{"id":5345,"date":"2016-03-03T16:26:14","date_gmt":"2016-03-03T15:26:14","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5345"},"modified":"2016-03-03T16:26:14","modified_gmt":"2016-03-03T15:26:14","slug":"lmf2016-deduccion-natural-proposicional-en-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2016-deduccion-natural-proposicional-en-isabellehol\/","title":{"rendered":"LMF2016: Deducci\u00f3n natural proposicional en Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-15\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha estudiado la formalizaci\u00f3n en Isabelle\/HOL de las demostraciones por deducci\u00f3n natural estudiadas en el <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-15\/temas\/tema-2.pdf\">tema 2<\/a>.<\/p>\n<p>Para cada uno de los ejemplos se ha presentado distintas demostraciones: detallada (que sea parecida a la mostrada en las transparencias), estructurada y autom\u00e1tica.<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter {* Tema 2: Deducci\u00f3n natural proposicional con Isabelle\/HOL *}\n\ntheory T2\nimports Main \nbegin\n\ntext {*\n  En esta secci\u00f3n 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 de \"L\u00f3gica inform\u00e1tica\" (LI) \n  http:\/\/goo.gl\/AwDiv\n \n  La p\u00e1gina al lado de cada ejemplo indica la p\u00e1gina de las transparencias \n  de LI 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\n\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\ntext {*\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"\u27e6 ... \u27e7\" para representar las hip\u00f3tesis,\n  \u00b7 \";\" para separar las hip\u00f3tesis y\n  \u00b7 \"\u27f9\" para separar las hip\u00f3tesis de la conclusi\u00f3n. *}\n\ntext {* Se puede hacer la demostraci\u00f3n por razonamiento hacia atr\u00e1s,\n  como sigue *}\n\nlemma ejemplo_1_6:\n  assumes \"p \u2227 q\" \n      and \"r\" \n  shows   \"q \u2227 r\"     \nproof (rule conjI)\n  show \"q\" using assms(1) by (rule conjunct2)\nnext\n  show \"r\" using assms(2) by this\nqed\n\ntext {*\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"proof (rule r)\" para indicar que se har\u00e1 la demostraci\u00f3n con la\n    regla r,\n  \u00b7 \"next\" para indicar el comienzo de la prueba del siguiente\n    subobjetivo,\n  \u00b7 \"this\" para indicar el hecho actual. *}\n\ntext {* Se pueden dejar impl\u00edcitas las reglas como sigue *}\n\nlemma ejemplo_1_7:\n  assumes \"p \u2227 q\" \n          \"r\" \n  shows   \"q \u2227 r\"     \nproof \n  show \"q\" using assms(1) ..\nnext\n  show \"r\" using assms(2) . \nqed\n\ntext {*\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \".\" para indicar por el hecho actual. *}\n\nsubsection {* Reglas de la doble negaci\u00f3n *}\n\ntext {*\n  La regla de eliminaci\u00f3n de la doble negaci\u00f3n es\n  \u00b7 notnotD: \u00ac\u00ac P \u27f9 P\n\n  Para ajustarnos al tema de LI vamos a introducir la siguiente regla de\n  introducci\u00f3n de la doble negaci\u00f3n\n  \u00b7 notnotI: P \u27f9 \u00ac\u00ac P\n  aunque, de momento, no detallamos su demostraci\u00f3n.\n*}\n\nlemma notnotI [intro!]: \"P \u27f9 \u00ac\u00ac P\"\nby auto\n\ntext {*\n  Ejemplo 2. (p. 5)\n       p, \u00ac\u00ac(q \u2227 r) \u22a2 \u00ac\u00acp \u2227 r\n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_2_1:\n  assumes 1: \"p\" and\n          2: \"\u00ac\u00ac(q \u2227 r)\" \n  shows      \"\u00ac\u00acp \u2227 r\"\nproof -\n  have 3: \"\u00ac\u00acp\" using 1 by (rule notnotI)\n  have 4: \"q \u2227 r\" using 2 by (rule notnotD)\n  have 5: \"r\" using 4 by (rule conjunct2)\n  show 6: \"\u00ac\u00acp \u2227 r\" using 3 5 by (rule conjI)\nqed        \n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_2_2:\n  assumes \"p\" \n          \"\u00ac\u00ac(q \u2227 r)\" \n  shows   \"\u00ac\u00acp \u2227 r\"\nproof -\n  have  \"\u00ac\u00acp\" using assms(1) ..\n  have  \"q \u2227 r\" using assms(2) by (rule notnotD)\n  hence \"r\" ..\n  with `\u00ac\u00acp` show  \"\u00ac\u00acp \u2227 r\" ..\nqed        \n\ntext {*\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"hence\" para indicar que se tiene por el hecho anterior y\n  \u00b7 `...` para referenciar un hecho. *}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_2_3:\n  assumes \"p\" \n          \"\u00ac\u00ac(q \u2227 r)\" \n  shows   \"\u00ac\u00acp \u2227 r\"\nusing assms\nby auto\n\ntext {* Se puede demostrar hacia atr\u00e1s *}\n\nlemma ejemplo_2_4:\n  assumes \"p\" \n          \"\u00ac\u00ac(q \u2227 r)\" \n  shows   \"\u00ac\u00acp \u2227 r\"\nproof  (rule conjI)\n  show \"\u00ac\u00acp\" using assms(1) by (rule notnotI)\nnext\n  have \"q \u2227 r\" using assms(2) by (rule notnotD) \n  thus \"r\" by (rule conjunct2)\nqed \n\ntext {* Se puede eliminar las reglas en la demostraci\u00f3n anterior, como\n  sigue: *}\n\nlemma ejemplo_2_5:\n  assumes \"p\" \n          \"\u00ac\u00ac(q \u2227 r)\" \n  shows   \"\u00ac\u00acp \u2227 r\"\nproof \n  show \"\u00ac\u00acp\" using assms(1) ..\nnext\n  have \"q \u2227 r\" using assms(2) by (rule notnotD) \n  thus \"r\" .. \nqed\n\nsubsection {* Regla de eliminaci\u00f3n del condicional *}\n\ntext {*\n  La regla de eliminaci\u00f3n del condicional es la regla del modus ponens\n  \u00b7 mp: \u27e6P \u27f6 Q; P\u27e7 \u27f9 Q \n*}\n\ntext {* \n  Ejemplo 3. (p. 6) Demostrar que\n     \u00acp \u2227 q, \u00acp \u2227 q \u27f6 r \u2228 \u00acp \u22a2 r \u2228 \u00acp\n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_3_1:\n  assumes 1: \"\u00acp \u2227 q\" and \n          2: \"\u00acp \u2227 q \u27f6 r \u2228 \u00acp\" \n  shows      \"r \u2228 \u00acp\"\nproof -\n  show \"r \u2228 \u00acp\" using 2 1 by (rule mp)\nqed    \n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_3_2:\n  assumes \"\u00acp \u2227 q\"\n          \"\u00acp \u2227 q \u27f6 r \u2228 \u00acp\" \n  shows   \"r \u2228 \u00acp\"\nproof -\n  show \"r \u2228 \u00acp\" using assms(2,1) ..\nqed    \n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_3_3:\n  assumes \"\u00acp \u2227 q\"\n          \"\u00acp \u2227 q \u27f6 r \u2228 \u00acp\" \n  shows   \"r \u2228 \u00acp\"\nusing assms\nby auto\n\ntext {* \n  Ejemplo 4 (p. 6) Demostrar que\n     p, p \u27f6 q, p \u27f6 (q \u27f6 r) \u22a2 r\n *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_4_1:\n  assumes 1: \"p\" and \n          2: \"p \u27f6 q\" and \n          3: \"p \u27f6 (q \u27f6 r)\" \n  shows \"r\"\nproof -\n  have 4: \"q\" using 2 1 by (rule mp)\n  have 5: \"q \u27f6 r\" using 3 1 by (rule mp)\n  show 6: \"r\" using 5 4 by (rule mp)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_4_2:\n  assumes \"p\"\n          \"p \u27f6 q\"\n          \"p \u27f6 (q \u27f6 r)\" \n  shows \"r\"\nproof -\n  have \"q\" using assms(2,1) .. \n  have \"q \u27f6 r\" using assms(3,1) ..\n  thus \"r\" using `q` ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_4_3:\n  \"\u27e6p; p \u27f6 q; p \u27f6 (q \u27f6 r)\u27e7 \u27f9 r\"\nby auto\n\nsubsection {* Regla derivada del modus tollens *}\n\ntext {*\n  Para ajustarnos al tema de LI vamos a introducir la regla del modus\n  tollens\n  \u00b7 mt: \u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF \n  aunque, de momento, sin detallar su demostraci\u00f3n.\n*}\n\nlemma mt: \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"\nby auto\n\ntext {*\n  Ejemplo 5 (p. 7). Demostrar\n     p \u27f6 (q \u27f6 r), p, \u00acr \u22a2 \u00acq\n *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_5_1:\n  assumes 1: \"p \u27f6 (q \u27f6 r)\" and \n          2: \"p\" and \n          3: \"\u00acr\" \n  shows \"\u00acq\"\nproof -\n  have 4: \"q \u27f6 r\" using 1 2 by (rule mp)\n  show \"\u00acq\" using 4 3 by (rule mt)\nqed    \n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_5_2:\n  assumes \"p \u27f6 (q \u27f6 r)\"\n          \"p\"\n          \"\u00acr\" \n  shows   \"\u00acq\"\nproof -\n  have \"q \u27f6 r\" using assms(1,2) ..\n  thus \"\u00acq\" using assms(3) by (rule mt)\nqed    \n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_5_3:\n  assumes \"p \u27f6 (q \u27f6 r)\"\n          \"p\"\n          \"\u00acr\" \n  shows   \"\u00acq\"\nusing assms\nby auto\n\ntext {* \n  Ejemplo 6. (p. 7) Demostrar \n     \u00acp \u27f6 q, \u00acq \u22a2 p\n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_6_1:\n  assumes 1: \"\u00acp \u27f6 q\" and \n          2: \"\u00acq\" \n  shows \"p\"\nproof -\n  have 3: \"\u00ac\u00acp\" using 1 2 by (rule mt)\n  show \"p\" using 3 by (rule notnotD)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_6_2:\n  assumes \"\u00acp \u27f6 q\"\n          \"\u00acq\" \n  shows   \"p\"\nproof -\n  have \"\u00ac\u00acp\" using assms(1,2) by (rule mt)\n  thus \"p\" by (rule notnotD)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_6_3:\n  \"\u27e6\u00acp \u27f6 q; \u00acq\u27e7 \u27f9 p\"\nby auto\n\ntext {* \n  Ejemplo 7. (p. 7) Demostrar\n     p \u27f6 \u00acq, q \u22a2 \u00acp\n  *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_7_1:\n  assumes 1: \"p \u27f6 \u00acq\" and \n          2: \"q\" \n  shows \"\u00acp\"\nproof -\n  have 3: \"\u00ac\u00acq\" using 2 by (rule notnotI)\n  show \"\u00acp\" using 1 3 by (rule mt)\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_7_2:\n  assumes \"p \u27f6 \u00acq\"\n          \"q\" \n  shows   \"\u00acp\"\nproof -\n  have \"\u00ac\u00acq\" using assms(2) by (rule notnotI)\n  with assms(1) show \"\u00acp\" by (rule mt)\nqed\n\ntext {*\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"with P show Q\" para indicar que con el hecho anterior junto con el\n    hecho P se demuestra Q. *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_7_3:\n  \"\u27e6p \u27f6 \u00acq; q\u27e7 \u27f9 \u00acp\"\nby auto\n\nsubsection {* Regla de introducci\u00f3n del condicional *}\n\ntext {*\n  La regla de introducci\u00f3n del condicional es\n  \u00b7 impI: (P \u27f9 Q) \u27f9 P \u27f6 Q\n*}\n\ntext {* \n  Ejemplo 8. (p. 8) Demostrar\n     p \u27f6 q \u22a2 \u00acq \u27f6 \u00acp\n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_8_1:\n  assumes 1: \"p \u27f6 q\" \n  shows \"\u00acq \u27f6 \u00acp\"\nproof -\n  { assume 2: \"\u00acq\"\n    have \"\u00acp\" using 1 2 by (rule mt) } \n  thus \"\u00acq \u27f6 \u00acp\" by (rule impI)\nqed    \n\ntext {*\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"{ ... }\" para representar una caja. *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_8_2:\n  assumes \"p \u27f6 q\" \n  shows \"\u00acq \u27f6 \u00acp\"\nproof \n  assume \"\u00acq\"\n  with assms show \"\u00acp\" by (rule mt)\nqed    \n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_8_3:\n  assumes \"p \u27f6 q\" \n  shows \"\u00acq \u27f6 \u00acp\"\nusing assms\nby auto\n\ntext {* \n  Ejemplo 9. (p. 9) Demostrar\n     \u00acq \u27f6 \u00acp \u22a2 p \u27f6 \u00ac\u00acq\n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_9_1: \n  assumes 1: \"\u00acq \u27f6 \u00acp\" \n  shows \"p \u27f6 \u00ac\u00acq\"   \nproof -\n  { assume 2: \"p\"\n    have 3: \"\u00ac\u00acp\" using 2 by (rule notnotI)\n    have \"\u00ac\u00acq\" using 1 3 by (rule mt) } \n  thus \"p \u27f6 \u00ac\u00acq\" by (rule impI)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_9_2:\n  assumes \"\u00acq \u27f6 \u00acp\" \n  shows    \"p \u27f6 \u00ac\u00acq\"   \nproof \n  assume \"p\"\n  hence \"\u00ac\u00acp\" by (rule notnotI)\n  with assms show \"\u00ac\u00acq\" by (rule mt)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_9_3:\n  assumes \"\u00acq \u27f6 \u00acp\" \n  shows \"p \u27f6 \u00ac\u00acq\"   \nusing assms\nby auto\n\ntext {* \n  Ejemplo 10 (p. 9). Demostrar\n     \u22a2 p \u27f6 p\n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_10_1:\n  \"p \u27f6 p\"\nproof -\n  { assume 1: \"p\"\n    have \"p\" using 1 by this }\n  thus \"p \u27f6 p\" by (rule impI) \nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejemplo_10_2:\n  \"p \u27f6 p\"\nproof (rule impI)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_10_3:\n  \"p \u27f6 p\"\nby auto\n\ntext {*\n  Ejemplo 11 (p. 10) Demostrar\n     \u22a2 (q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\n *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejemplo_11_1:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\nproof -\n  { assume 1: \"q \u27f6 r\"\n    { assume 2: \"\u00acq \u27f6 \u00acp\"\n      { assume 3: \"p\"\n        have 4: \"\u00ac\u00acp\" using 3 by (rule notnotI)\n        have 5: \"\u00ac\u00acq\" using 2 4 by (rule mt)\n        have 6: \"q\" using 5 by (rule notnotD)\n        have \"r\" using 1 6 by (rule mp) } \n      hence \"p \u27f6 r\" by (rule impI) } \n    hence \"(\u00acq \u27f6 \u00acp) \u27f6 p \u27f6 r\" by (rule impI) } \n  thus \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 p \u27f6 r)\" by (rule impI)\nqed\n\n-- \"La demostraci\u00f3n hacia atr\u00e1s es\"\nlemma ejemplo_11_2:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\nproof (rule impI)\n  assume 1: \"q \u27f6 r\"\n  show \"(\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r)\"\n  proof (rule impI)\n    assume 2: \"\u00acq \u27f6 \u00acp\"\n    show \"p \u27f6 r\"\n    proof (rule impI)\n      assume 3: \"p\"\n      have 4: \"\u00ac\u00acp\" using 3 by (rule notnotI)\n      have 5: \"\u00ac\u00acq\" using 2 4 by (rule mt)\n      have 6: \"q\" using 5 by (rule notnotD)\n      show \"r\" using 1 6 by (rule mp)\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n hacia atr\u00e1s con reglas impl\u00edcitas es\"\nlemma ejemplo_11_3:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\nproof\n  assume 1: \"q \u27f6 r\"\n  show \"(\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r)\"\n  proof\n    assume 2: \"\u00acq \u27f6 \u00acp\"\n    show \"p \u27f6 r\"\n    proof\n      assume 3: \"p\"\n      have 4: \"\u00ac\u00acp\" using 3 ..\n      have 5: \"\u00ac\u00acq\" using 2 4 by (rule mt)\n      have 6: \"q\" using 5 by (rule notnotD)\n      show \"r\" using 1 6 ..\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n sin etiquetas es\" \nlemma ejemplo_11_4:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\nproof\n  assume \"q \u27f6 r\"\n  show \"(\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r)\"\n  proof\n    assume \"\u00acq \u27f6 \u00acp\"\n    show \"p \u27f6 r\"\n    proof\n      assume \"p\"\n      hence \"\u00ac\u00acp\" ..\n      with `\u00acq \u27f6 \u00acp` have \"\u00ac\u00acq\" by (rule mt)\n      hence \"q\" by (rule notnotD)\n      with `q \u27f6 r` show \"r\" ..\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejemplo_11_5:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\nby auto\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se ha estudiado la formalizaci\u00f3n en Isabelle\/HOL de las demostraciones por deducci\u00f3n natural estudiadas en el tema 2. Para cada uno de los ejemplos se ha presentado distintas demostraciones: detallada (que sea parecida a la mostrada en las transparencias), estructurada y autom\u00e1tica. La teor\u00eda&#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":[256],"tags":[144,312,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\/5345"}],"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=5345"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5345\/revisions"}],"predecessor-version":[{"id":5346,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5345\/revisions\/5346"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5345"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5345"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5345"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}