{"id":6898,"date":"2019-12-12T12:28:54","date_gmt":"2019-12-12T11:28:54","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6898"},"modified":"2019-12-15T12:30:52","modified_gmt":"2019-12-15T11:30:52","slug":"ra2019-deduccion-natural-proposicional-con-isabelle-hol-1","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-deduccion-natural-proposicional-con-isabelle-hol-1\/","title":{"rendered":"RA2019: Deducci\u00f3n natural proposicional con Isabelle\/HOL (1)"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-19\">Razonamiento autom\u00e1tico<\/a> se ha comenzado la presentaci\u00f3n de la deducci\u00f3n natural con Isabelle\/HOL.<\/p>\n<p>La presentaci\u00f3n se basa en los ejemplos del <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-14\/temas\/tema-2.pdf\">tema 2<\/a> del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/li-14\">L\u00f3gica inform\u00e1tica<\/a> que, a su vez, se basa en el cap\u00edtulo 2 del libro de Huth y Ryan <a href=\"http:\/\/goo.gl\/fGsqf\">Logic in Computer Science (Modelling and reasoning about systems)<\/a>.<\/p>\n<p>La p\u00e1gina al lado de cada ejemplo indica la p\u00e1gina de las transparencias donde se encuentra la demostraci\u00f3n.<\/p>\n<p>Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostraci\u00f3n de las transparencias, las siguientes van eliminando detalles de la prueba hasta la pen\u00faltima que es autom\u00e1tica y la \u00faltima es aplicativa.<\/p>\n<p>A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.<\/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 \u2039Tema 6: Deducci\u00f3n natural proposicional con Isabelle\/HOL\u203a\n\ntheory T6_Deduccion_natural_en_logica_proposicional_con_Isabelle\nimports Main \nbegin\n\nsection \u2039Reglas de la conjunci\u00f3n\u203a\n\nsubsection \u2039Ejemplo 1\u203a\n\ntext \u2039Ejemplo 1 (p. 4). Demostrar que\n     p \u2227 q, r \u22a2 q \u2227 r.\n\u203a     \n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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 \u2039Notas 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\u203a\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\ntext \u2039Se pueden dejar impl\u00edcitas las reglas como sigue\u203a\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 \u2039Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"..\" para indicar que se prueba por la regla correspondiente.\u203a\n\ntext \u2039Se pueden eliminar las etiquetas como sigue\u203a\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  then show \"q \u2227 r\" using assms(2) ..\nqed\n\ntext \u2039\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 \"then show\" para demostrar la conclusi\u00f3n usando el hecho anterior.\n  Adem\u00e1s, no es necesario usar and entre las hip\u00f3tesis.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\ntext \u2039Se puede automatizar la demostraci\u00f3n como sigue\u203a\n  \nlemma ejemplo_1_4:\n  assumes \"p \u2227 q\" \n          \"r\" \n  shows   \"q \u2227 r\"     \n  using assms\n  by auto\n\ntext \u2039Nota 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.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada hacia atr\u00e1s\u203a\n\ntext \u2039Se puede hacer la demostraci\u00f3n por razonamiento hacia atr\u00e1s,\n  como sigue\u203a\n\nlemma ejemplo_1_5:\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 \u2039Nota 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.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n estructurada hacia atr\u00e1s\u203a\n\ntext \u2039Se pueden dejar impl\u00edcitas las reglas como sigue\u203a\n\nlemma ejemplo_1_6:\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 \u2039Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \".\" para indicar por el hecho actual.\u203a\n\nsubsubsection \u2039Demostraciones autom\u00e1ticas\u203a\n\nlemma ejemplo_1_7:\n  assumes \"p \u2227 q\" \n          \"r\" \n  shows   \"q \u2227 r\"     \n  using assms by simp\n\n\u2015 \u2039Se puede acortar como sigue\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_1_8_:\n  \"\u27e6p \u2227 q; r\u27e7 \u27f9 q \u2227 r\"\n  by simp\n\ntext \u2039Nota 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.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\n\u2015 \u2039La demostraci\u00f3n aplicativa es\u203a\nlemma ejemplo_1_9: \n  \"\u27e6p \u2227 q; r\u27e7 \u27f9 q \u2227 r\"\n  apply (rule conjI)\n   apply (erule conjunct2)\n  apply assumption  \n  done \n\ntext \u2039Explicaciones:\n  apply (rule conjI)\n  + Objetivo:         \u27e6p \u2227 q; r\u27e7 \u27f9 q \u2227 r\n  + conjI:            \u27e6?P; ?Q\u27e7 \u27f9 ?P \u2227 ?Q\n  + Unificador de     q \u2227 r\n    y                 ?P \u2227 ?Q\n    es                ?P\/q, ?Q\/r\n  + Nuevos objetivos: \u27e6p \u2227 q; r\u27e7 \u27f9 q\n                      \u27e6p \u2227 q; r\u27e7 \u27f9 r  \n\n  apply (erule conjunct2)\n  + Objetivo:         \u27e6p \u2227 q; r\u27e7 \u27f9 q\n  + conjunct2:        ?P \u2227 ?Q \u27f9 ?Q\n  + Unificador de     p \u2227 q\n    y                 ?P \u2227 ?Q\n    es                ?P\/p, ?Q\/q\n  + Nuevo objetivo:   Nada  \n\u203a\n\nsection \u2039Reglas de la doble negaci\u00f3n\u203a\n\nsubsection \u2039Reglas de la doble negaci\u00f3n\u203a\n\ntext \u2039La 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\u203a\n\nlemma notnotI [intro!]: \"P \u27f9 \u00ac\u00ac P\"\n  by auto\n\nsubsection \u2039Ejemplo 2\u203a\n\ntext \u2039Ejemplo 2. (p. 5)\n       p, \u00ac\u00ac(q \u2227 r) \u22a2 \u00ac\u00acp \u2227 r\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039Se puede eliminar etiquetas y reglas\u203a\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  then have \"r\" ..\n  with \u2039\u00ac\u00acp\u203a show  \"\u00ac\u00acp \u2227 r\" ..\nqed        \n\ntext \u2039Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 `...` para referenciar un hecho y\n  \u00b7 \"with P show Q\" para indicar que con el hecho anterior junto con el\n    hecho P se demuestra Q.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada hacia atr\u00e1s\u203a\n\ntext \u2039Se puede demostrar hacia atr\u00e1s\u203a\n\nlemma ejemplo_2_3:\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  then show \"r\" by (rule conjunct2)\nqed \n\nsubsubsection \u2039Demostraci\u00f3n estructurada hacia atr\u00e1s\u203a\n\ntext \u2039Se puede eliminar las reglas en la demostraci\u00f3n anterior, como\n  sigue:\u203a\n\nlemma ejemplo_2_4:\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  then show \"r\" .. \nqed\n\nsubsubsection \u2039Demostraciones autom\u00e1ticas\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_2_5:\n  assumes \"p\" \n          \"\u00ac\u00ac(q \u2227 r)\" \n  shows   \"\u00ac\u00acp \u2227 r\"\n  using assms\n  by simp\n\n\u2015 \u2039Se puede simplificar\u203a\nlemma ejemplo_2_6: \n  \"\u27e6p; \u00ac\u00ac(q \u2227 r)\u27e7 \u27f9 \u00ac\u00acp \u2227 r\"\n  by simp\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_2_7: \n  \"\u27e6p; \u00ac\u00ac(q \u2227 r)\u27e7 \u27f9 \u00ac\u00acp \u2227 r\"\n  apply (rule conjI)\n   apply (rule notnotI)\n   apply assumption\n  apply (drule notnotD)\n  apply (erule conjunct2)\n  done\n\ntext \u2039Explicaciones:\n  apply (rule conjI)\n  + Objetivo:         \u27e6p; \u00ac\u00ac(q \u2227 r)\u27e7 \u27f9 \u00ac\u00acp \u2227 r\n  + conjI:            \u27e6?P; ?Q\u27e7 \u27f9 ?P \u2227 ?Q\n  + Unificador de     \u00ac\u00acp \u2227 r\n    y                 ?P \u2227 ?Q\n    es                ?P\/\u00ac\u00acp, ?Q\/r\n  + Nuevos objetivos: \u27e6p; \u00ac \u00ac (q \u2227 r)\u27e7 \u27f9 \u00ac \u00ac p\n                      \u27e6p; \u00ac \u00ac (q \u2227 r)\u27e7 \u27f9 r  \n\n  apply (rule notnotI)\n  + Objetivo:         \u27e6p; \u00ac \u00ac (q \u2227 r)\u27e7 \u27f9 \u00ac \u00ac p\n  + notnotI:          ?P \u27f9 \u00ac \u00ac ?P\n  + Unificador de     \u00ac \u00ac p\n    y                 \u00ac \u00ac ?P\n    es                ?P\/p\n  + Nuevo objetivo:   \u27e6p; \u00ac \u00ac (q \u2227 r)\u27e7 \u27f9 p  \n\n  apply (drule notnotD)\n  + Objetivo:         \u27e6p; \u00ac \u00ac (q \u2227 r)\u27e7 \u27f9 r\n  + notnotD:          \u00ac \u00ac ?P \u27f9 ?P\n  + Unificador de     \u00ac \u00ac (q \u2227 r)\n    y                 \u00ac \u00ac ?P\n    es                ?P\/(q \u2227 r)\n  + Nuevo objetivo:   \u27e6p; q \u2227 r\u27e7 \u27f9 r  \n\n  apply (erule conjunct2)\n  + Objetivo:         \u27e6p; q \u2227 r\u27e7 \u27f9 r\n  + conjunct2:        ?P \u2227 ?Q \u27f9 ?Q\n  + Unificador de     q \u2227 r\n    y                 ?P \u2227 ?Q\n    es                ?P\/q, ?Q\/r\n  + Nuevo objetivo:   Nada  \n\u203a\n\nsection \u2039Regla de eliminaci\u00f3n del condicional\u203a\n\ntext \u2039La regla de eliminaci\u00f3n del condicional es la regla del modus \n  ponens\n  \u00b7 mp: \u27e6P \u27f6 Q; P\u27e7 \u27f9 Q \n\u203a\n\nsubsection \u2039Ejemplo 3\u203a\n\ntext \u2039Ejemplo 3. (p. 6) Demostrar que\n     \u00acp \u2227 q, \u00acp \u2227 q \u27f6 r \u2228 \u00acp \u22a2 r \u2228 \u00acp\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_3_3: \n  \"\u27e6\u00acp \u2227 q; \u00acp \u2227 q \u27f6 r \u2228 \u00acp\u27e7 \u27f9 r \u2228 \u00acp\"\n  apply (erule mp)\n  apply assumption\n  done\n\ntext \u2039Explicaciones:\n  apply (erule mp)\n  + Objetivo:         \u27e6\u00acp \u2227 q; \u00acp \u2227 q \u27f6 r \u2228 \u00acp\u27e7 \u27f9 r \u2228 \u00acp\n  + mp:               \u27e6?P \u27f6 ?Q; ?P\u27e7 \u27f9 ?Q\n  + Unificador de     \u00acp \u2227 q \u27f6 r \u2228 \u00acp \n    y                 ?P \u27f6 ?Q\n    es                ?P\/\u00acp \u2227 q, ?Q\/r \u2228 \u00acp\n  + Nuevos objetivos: \u00ac p \u2227 q \u27f9 \u00ac p \u2227 q  \n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_3_4:\n  \"\u27e6\u00acp \u2227 q; \u00acp \u2227 q \u27f6 r \u2228 \u00acp\u27e7 \u27f9 r \u2228 \u00acp\"\n  by simp\n\nsubsection \u2039Ejemplo 4\u203a\n\ntext \u2039\n  Ejemplo 4 (p. 6) Demostrar que\n     p, p \u27f6 q, p \u27f6 (q \u27f6 r) \u22a2 r\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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  then show \"r\" using \u2039q\u203a ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_4_3:\n  \"\u27e6p; p \u27f6 q; p \u27f6 (q \u27f6 r)\u27e7 \u27f9 r\"\n  apply (drule mp)\n   apply assumption\n  apply (drule mp)\n   apply assumption\n  apply (drule mp)\n   apply assumption+\n  done    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_4_4:\n  \"\u27e6p; p \u27f6 q; p \u27f6 (q \u27f6 r)\u27e7 \u27f9 r\"\n  by simp\n\nsection \u2039Regla derivada del modus tollens\u203a\n\ntext \u2039Para ajustarnos al tema de LI vamos a introducir la regla del \n  modus tollens\n  \u00b7 mt: \u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF \n  aunque, de momento, sin detallar su demostraci\u00f3n.\u203a\n\nlemma mt: \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"\n  by simp\n\nsubsection \u2039Ejemplo 5\u203a\n\ntext \u2039Ejemplo 5 (p. 7). Demostrar\n     p \u27f6 (q \u27f6 r), p, \u00acr \u22a2 \u00acq\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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  then show \"\u00acq\" using assms(3) by (rule mt)\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_5_3:\n  assumes \"p \u27f6 (q \u27f6 r)\"\n          \"p\"\n          \"\u00acr\" \n  shows   \"\u00acq\"\n  using assms\n  by simp\n\nlemma ejemplo_5_4: \n  \"\u27e6p \u27f6 (q \u27f6 r); p; \u00acr \u27e7 \u27f9 \u00acq\"\n  by simp\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_5_5: \n  \"\u27e6p \u27f6 (q \u27f6 r); p; \u00acr \u27e7 \u27f9 \u00acq\"\n  apply (drule mp)\n   apply assumption\n  apply (erule mt)\n  apply assumption\n  done\n\nsubsection \u2039Ejemplo 6\u203a\n\ntext \u2039Ejemplo 6. (p. 7) Demostrar \n     \u00acp \u27f6 q, \u00acq \u22a2 p\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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  then show \"p\" by (rule notnotD)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_6_3:\n  \"\u27e6\u00acp \u27f6 q; \u00acq\u27e7 \u27f9 p\"\n  by simp\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_6_4: \n  \"\u27e6\u00acp \u27f6 q; \u00acq\u27e7 \u27f9 p\"  \n  apply (drule mt)\n   apply assumption\n  apply (erule notnotD)\n  done\n\nsubsection \u2039Ejemplo 7\u203a\n\ntext \u2039Ejemplo 7. (p. 7) Demostrar\n     p \u27f6 \u00acq, q \u22a2 \u00acp\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_7_3:\n  \"\u27e6p \u27f6 \u00acq; q\u27e7 \u27f9 \u00acp\"\n  by simp\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_7_4: \n  \"\u27e6p \u27f6 \u00acq; q\u27e7 \u27f9 \u00acp\"  \n  apply (erule mt)\n  apply (erule notnotI)\n  done\n\nsection \u2039Regla de introducci\u00f3n del condicional\u203a\n\ntext \u2039La regla de introducci\u00f3n del condicional es\n  \u00b7 impI: (P \u27f9 Q) \u27f9 P \u27f6 Q\n\u203a\n\nsubsection \u2039Ejemplo 8\u203a\n\ntext \u2039  Ejemplo 8. (p. 8) Demostrar\n     p \u27f6 q \u22a2 \u00acq \u27f6 \u00acp\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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  then show \"\u00acq \u27f6 \u00acp\" by (rule impI)\nqed    \n\ntext \u2039\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"{ ... }\" para representar una caja.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\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\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_8_3:\n  assumes \"p \u27f6 q\" \n  shows \"\u00acq \u27f6 \u00acp\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\nlemma ejemplo_8_4: \n  \"p \u27f6 q \u27f9 \u00acq \u27f6 \u00acp\"\n  apply (rule impI)\n  apply (erule mt)\n  apply assumption\n  done\n\nsubsection \u2039Ejemplo 9\u203a\n\ntext \u2039Ejemplo 9. (p. 9) Demostrar\n     \u00acq \u27f6 \u00acp \u22a2 p \u27f6 \u00ac\u00acq\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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  then show \"p \u27f6 \u00ac\u00acq\" by (rule impI)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_9_2:\n  assumes \"\u00acq \u27f6 \u00acp\" \n  shows    \"p \u27f6 \u00ac\u00acq\"   \nproof \n  assume \"p\"\n  then have \"\u00ac\u00acp\" by (rule notnotI)\n  with assms show \"\u00ac\u00acq\" by (rule mt)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_9_3:\n  assumes \"\u00acq \u27f6 \u00acp\" \n  shows \"p \u27f6 \u00ac\u00acq\"   \n  using assms\n  by auto \n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_9_4: \n  \"\u00acq \u27f6 \u00acp \u27f9 p \u27f6 \u00ac\u00acq\"  \n  apply (rule impI)\n  apply (erule mt)\n  apply (rule notnotI)\n  apply assumption\n  done\n\nsubsection \u2039Ejemplo 10\u203a\n\ntext \u2039Ejemplo 10 (p. 9). Demostrar\n     \u22a2 p \u27f6 p\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_10_1:\n  \"p \u27f6 p\"\nproof -\n  { assume 1: \"p\"\n    have \"p\" using 1 by this }\n  then show \"p \u27f6 p\" by (rule impI) \nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_10_2:\n  \"p \u27f6 p\"\nproof (rule impI)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_10_3:\n  \"p \u27f6 p\"\n  by simp \n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_10_4: \n  \"p \u27f6 p\"\n  apply (rule impI)\n  apply assumption\n  done\n\nsubsection \u2039Ejemplo 11\u203a\n\ntext \u2039Ejemplo 11 (p. 10) Demostrar\n     \u22a2 (q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\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      then have \"p \u27f6 r\" by (rule impI) } \n    then have \"(\u00acq \u27f6 \u00acp) \u27f6 p \u27f6 r\" by (rule impI) } \n  then show \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 p \u27f6 r)\" by (rule impI)\nqed\n\n\u2015 \u2039La demostraci\u00f3n hacia atr\u00e1s es\u203a\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\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n hacia atr\u00e1s con reglas impl\u00edcitas es\u203a\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\u2015 \u2039La demostraci\u00f3n sin etiquetas es\u203a \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      then have \"\u00ac\u00acp\" ..\n      with \u2039\u00acq \u27f6 \u00acp\u203a have \"\u00ac\u00acq\" by (rule mt)\n      then have \"q\" by (rule notnotD)\n      with \u2039q \u27f6 r\u203a show \"r\" ..\n    qed\n  qed\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_11_5:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_11_6:\n  \"(q \u27f6 r) \u27f6 ((\u00acq \u27f6 \u00acp) \u27f6 (p \u27f6 r))\"  \n  apply (rule impI)+  \n  apply (erule mp)\n  apply (drule mt)\n   apply (rule notnotI)\n   apply assumption\n  apply (rule notnotD)\n  apply assumption\n  done\n\nend\n<\/pre>\n<p>Como pr\u00e1ctica, se ha propuesto la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/RA2019\/index.php\/R6\">6\u00aa relaci\u00f3n de ejercicios<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se ha comenzado la presentaci\u00f3n de la deducci\u00f3n natural con Isabelle\/HOL. La presentaci\u00f3n se basa en los ejemplos del tema 2 del curso de L\u00f3gica inform\u00e1tica que, a su vez, se basa en el cap\u00edtulo 2 del libro de Huth y Ryan Logic in Computer&#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":[333],"tags":[],"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\/6898"}],"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=6898"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6898\/revisions"}],"predecessor-version":[{"id":6900,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6898\/revisions\/6900"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6898"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6898"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6898"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}