{"id":6902,"date":"2019-12-19T11:56:50","date_gmt":"2019-12-19T10:56:50","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6902"},"modified":"2019-12-20T11:57:44","modified_gmt":"2019-12-20T10:57:44","slug":"ra2019-deduccion-natural-proposicional-con-isabelle-hol-2","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-deduccion-natural-proposicional-con-isabelle-hol-2\/","title":{"rendered":"RA2019: Deducci\u00f3n natural proposicional con Isabelle\/HOL (2)"},"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 completado 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 disyunci\u00f3n\u203a\n\ntext \u2039\n  Las reglas de la introducci\u00f3n de la disyunci\u00f3n son\n  \u00b7 disjI1: P \u27f9 P \u2228 Q\n  \u00b7 disjI2: Q \u27f9 P \u2228 Q\n  La regla de elimaci\u00f3n de la disyunci\u00f3n es\n  \u00b7 disjE:  \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R \n\u203a\n\nsubsection \u2039Ejemplo 12\u203a\n\ntext \u2039Ejemplo 12 (p. 11). Demostrar\n     p \u2228 q \u22a2 q \u2228 p\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_12_1:\n  assumes \"p \u2228 q\" \n  shows \"q \u2228 p\"\nproof -\n  have \"p \u2228 q\" using assms by this\n  moreover\n  { assume 2: \"p\"\n    have \"q \u2228 p\" using 2 by (rule disjI2) }\n  moreover\n  { assume 3: \"q\"\n    have \"q \u2228 p\" using 3 by (rule disjI1) }\n  ultimately show \"q \u2228 p\" by (rule disjE) \nqed    \n\ntext \u2039\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"moreover\" para separar los bloques y\n  \u00b7 \"ultimately\" para unir los resultados de los bloques.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada con reglas impl\u00edcitas es\u203a\nlemma ejemplo_12_2:\n  assumes \"p \u2228 q\" \n  shows \"q \u2228 p\"\nproof -\n  note \u2039p \u2228 q\u203a\n  moreover\n  { assume \"p\"\n    then have \"q \u2228 p\" .. }\n  moreover\n  { assume \"q\"\n    then have \"q \u2228 p\" .. }\n  ultimately show \"q \u2228 p\" ..\nqed    \n\ntext \u2039\n  Nota sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"note\" para copiar un hecho.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada hacia atr\u00e1s\u203a\n\n\u2015 \u2039La demostraci\u00f3n hacia atr\u00e1s es\u203a\nlemma ejemplo_12_3:\n  assumes 1: \"p \u2228 q\" \n  shows \"q \u2228 p\"\nusing 1\nproof (rule disjE)\n  { assume 2: \"p\"\n    show \"q \u2228 p\" using 2 by (rule disjI2) }\nnext\n  { assume 3: \"q\"\n    show \"q \u2228 p\" using 3 by (rule disjI1) }\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada hacia atr\u00e1s\u203a\n\n\u2015 \u2039La demostraci\u00f3n hacia atr\u00e1s con reglas impl\u00edcitas es\u203a\nlemma ejemplo_12_4:\n  assumes \"p \u2228 q\" \n  shows \"q \u2228 p\"\nusing assms\nproof \n  { assume  \"p\"\n    then show \"q \u2228 p\" .. }\nnext\n  { assume \"q\"\n    then show \"q \u2228 p\" .. }\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_12_5:\n  assumes \"p \u2228 q\" \n  shows \"q \u2228 p\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_12_6: \n  \"p \u2228 q \u27f9 q \u2228 p\"  \n  apply (erule disjE)\n   apply (rule disjI2)\n   prefer 2\n   apply (rule disjI1)\n   apply assumption+ \n  done\n\nsubsection \u2039Ejemplo 13\u203a\n\ntext \u2039\n  Ejemplo 13. (p. 12) Demostrar\n     q \u27f6 r \u22a2 p \u2228 q \u27f6 p \u2228 r\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a \nlemma ejemplo_13_1:\n  assumes 1: \"q \u27f6 r\"\n  shows \"p \u2228 q \u27f6 p \u2228 r\"\nproof (rule impI)\n  assume 2: \"p \u2228 q\"\n  then show \"p \u2228 r\"\n  proof (rule disjE)\n    { assume 3: \"p\"\n      show \"p \u2228 r\" using 3 by (rule disjI1) }\n  next\n    { assume 4: \"q\"\n      have 5: \"r\" using 1 4 by (rule mp)\n      show \"p \u2228 r\" using 5 by (rule disjI2) }\n  qed\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a \nlemma ejemplo_13_2:\n  assumes \"q \u27f6 r\"\n  shows \"p \u2228 q \u27f6 p \u2228 r\"\nproof \n  assume \"p \u2228 q\"\n  then show \"p \u2228 r\"\n  proof \n    { assume \"p\"\n      then show \"p \u2228 r\" .. }\n  next\n    { assume \"q\"\n      have \"r\" using assms \u2039q\u203a ..\n      then show \"p \u2228 r\" .. }\n  qed\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a \nlemma ejemplo_13_3:\n  assumes \"q \u27f6 r\"\n  shows \"p \u2228 q \u27f6 p \u2228 r\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_13_4: \n  \"q \u27f6 r \u27f9 p \u2228 q \u27f6 p \u2228 r\"  \n  apply (rule impI)\n  apply (erule disjE)\n   apply (rule disjI1)\n   prefer 2\n   apply (drule mp)\n  prefer 2\n    apply (rule disjI2)\n    apply assumption+\n  done\n\nsection \u2039Regla de copia\u203a\n\nsubsection \u2039Ejemplo 14\u203a\n\ntext \u2039Ejemplo 14 (p. 13). Demostrar\n     \u22a2 p \u27f6 (q \u27f6 p)\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_14_1:\n  \"p \u27f6 (q \u27f6 p)\"\nproof (rule impI)\n  assume 1: \"p\"\n  show \"q \u27f6 p\" \n  proof (rule impI)\n    assume \"q\"\n    show \"p\" using 1 by this\n  qed\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_14_2:\n  \"p \u27f6 (q \u27f6 p)\"\nproof \n  assume \"p\"\n  then show \"q \u27f6 p\" ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_14_3:\n  \"p \u27f6 (q \u27f6 p)\"\n  by simp \n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_14_4: \n  \"p \u27f6 (q \u27f6 p)\"  \n  apply (rule impI)+\n  apply assumption\n  done\n\nsection \u2039Reglas de la negaci\u00f3n\u203a\n\ntext \u2039La regla de eliminaci\u00f3n de lo falso es\n  \u00b7 FalseE: False \u27f9 P\n  La regla de eliminaci\u00f3n de la negaci\u00f3n es\n  \u00b7 notE: \u27e6\u00acP; P\u27e7 \u27f9 R\n  La regla de introducci\u00f3n de la negaci\u00f3n es\n  \u00b7 notI: (P \u27f9 False) \u27f9 \u00acP\n\u203a\n\nsubsection \u2039Ejemplo 15\u203a\n\ntext \u2039Ejemplo 15 (p. 15). Demostrar\n     \u00acp \u2228 q \u22a2 p \u27f6 q\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_15_1:\n  assumes 1: \"\u00acp \u2228 q\" \n  shows \"p \u27f6 q\"\nproof (rule impI)\n  assume 2: \"p\"\n  note 1\n  then show \"q\"\n  proof (rule disjE)\n    { assume 3: \"\u00acp\"\n      show \"q\" using 3 2 by (rule notE) }\n  next\n    { assume 4: \"q\"\n      show \"q\" using 4 by this}\n  qed\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_15_2:\n  assumes \"\u00acp \u2228 q\" \n  shows \"p \u27f6 q\"\nproof \n  assume \"p\"\n  note \u2039\u00acp \u2228 q\u203a\n  then show \"q\"\n  proof\n    assume \"\u00acp\"\n    then show \"q\" using \u2039p\u203a .. \n  next\n    assume \"q\"\n      then show \"q\" .\n  qed\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_15_3:\n  assumes \"\u00acp \u2228 q\" \n  shows \"p \u27f6 q\"\n  using assms\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_15_4: \n  \"\u00acp \u2228 q \u27f9 p \u27f6 q\"  \n  apply (rule impI)\n  apply (erule disjE)\n   apply (erule notE)\n   apply assumption+\n  done\n\nsubsection \u2039Ejemplo 16\u203a\n\ntext \u2039Ejemplo 16 (p. 16). Demostrar\n     p \u27f6 q, p \u27f6 \u00acq \u22a2 \u00acp\n\u203a\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_16_1:\n  assumes 1: \"p \u27f6 q\" and \n          2: \"p \u27f6 \u00acq\" \n  shows \"\u00acp\"    \nproof (rule notI)\n  assume 3: \"p\"\n  have 4: \"q\" using 1 3 by (rule mp)\n  have 5: \"\u00acq\" using 2 3 by (rule mp)\n  show False using 5 4 by (rule notE)\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_16_2:\n  assumes \"p \u27f6 q\"\n          \"p \u27f6 \u00acq\" \n  shows \"\u00acp\"    \nproof \n  assume \"p\"\n  have \"q\" using assms(1) \u2039p\u203a ..\n  have \"\u00acq\" using assms(2) \u2039p\u203a ..\n  then show False using \u2039q\u203a ..\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_16_3:\n  assumes \"p \u27f6 q\"\n          \"p \u27f6 \u00acq\" \n  shows \"\u00acp\"    \n  using assms\n  by simp \n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_16_4: \n  \"\u27e6p \u27f6 q; p \u27f6 \u00acq\u27e7 \u27f9 \u00acp\"  \n  apply (rule notI)\n  apply (drule mp)+\n    apply assumption+\n  apply (drule mp)\n    prefer 2\n   apply (erule notE)\n   apply assumption+\n  done\n\nsection \u2039Reglas del bicondicional\u203a\n\ntext \u2039La regla de introducci\u00f3n del bicondicional es\n  \u00b7 iffI: \u27e6P \u27f9 Q; Q \u27f9 P\u27e7 \u27f9 P \u27f7 Q\n  Las reglas de eliminaci\u00f3n del bicondicional son\n  \u00b7 iffD1: \u27e6Q \u27f7 P; Q\u27e7 \u27f9 P \n  \u00b7 iffD2: \u27e6P \u27f7 Q; Q\u27e7 \u27f9 P\n\u203a\n\nsubsection \u2039Ejemplo 17\u203a\n\ntext \u2039Ejemplo 17 (p. 17) Demostrar\n     (p \u2227 q) \u27f7 (q \u2227 p)\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_17_1:\n  \"(p \u2227 q) \u27f7 (q \u2227 p)\" \nproof (rule iffI)\n  { assume 1: \"p \u2227 q\"\n    have 2: \"p\" using 1 by (rule conjunct1)\n    have 3: \"q\" using 1 by (rule conjunct2)\n    show \"q \u2227 p\" using 3 2 by (rule conjI) }\nnext\n  { assume 4: \"q \u2227 p\"\n    have 5: \"q\" using 4 by (rule conjunct1)\n    have 6: \"p\" using 4 by (rule conjunct2)\n    show \"p \u2227 q\" using 6 5 by (rule conjI) }\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_17_2:\n  \"(p \u2227 q) \u27f7 (q \u2227 p)\"\nproof \n  { assume 1: \"p \u2227 q\"\n    have \"p\" using 1 ..\n    have \"q\" using 1 ..\n    show \"q \u2227 p\" using \u2039q\u203a \u2039p\u203a .. }\nnext\n  { assume 2: \"q \u2227 p\"\n    have \"q\" using 2 ..\n    have \"p\" using 2 ..\n    show \"p \u2227 q\" using \u2039p\u203a \u2039q\u203a  .. }\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_17_3:\n  \"(p \u2227 q) \u27f7 (q \u2227 p)\"\n  by auto\n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_17_4: \n  \"(p \u2227 q) \u27f7 (q \u2227 p)\"  \n  apply (rule iffI)\n   apply (rule conjI)\n    apply (erule conjunct2)\n   apply (erule conjunct1)\n    apply (rule conjI)\n    apply (erule conjunct2)\n  apply (erule conjunct1)\n  done\n\nsubsection \u2039Ejemplo 18\u203a\n\ntext \u2039Ejemplo 18 (p. 18). Demostrar\n     p \u27f7 q, p \u2228 q \u22a2 p \u2227 q\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_18_1:\n  assumes 1: \"p \u27f7 q\" and \n          2: \"p \u2228 q\"  \n  shows \"p \u2227 q\"\nusing 2\nproof (rule disjE)\n  { assume 3: \"p\"\n    have 4: \"q\" using 1 3 by (rule iffD1)\n    show \"p \u2227 q\" using 3 4 by (rule conjI) }\nnext\n  { assume 5: \"q\"\n    have 6: \"p\" using 1 5 by (rule iffD2)\n    show \"p \u2227 q\" using 6 5 by (rule conjI) }\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_18_2:\n  assumes \"p \u27f7 q\"\n          \"p \u2228 q\"  \n  shows  \"p \u2227 q\"\nusing assms(2)\nproof\n  { assume \"p\"\n    with assms(1) have \"q\" ..\n    with \u2039p\u203a show \"p \u2227 q\" .. }\nnext\n  { assume \"q\"\n    with assms(1) have \"p\" ..\n    then show \"p \u2227 q\" using \u2039q\u203a .. }\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_18_3:\n  assumes \"p \u27f7 q\"\n          \"p \u2228 q\"  \n  shows \"p \u2227 q\"\n  using assms\n  by simp \n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_18_4: \n  \"\u27e6p \u27f7 q; p \u2228 q\u27e7 \u27f9 p \u2227 q\"  \n  apply (erule disjE)\n   apply (rule conjI)\n    apply assumption\n    apply (erule iffD1)\n    apply assumption\n    apply (rule conjI)\n    apply (erule iffD2)\n   apply assumption+\n  done\n\nsection \u2039Reglas derivadas\u203a\n\nsubsection \u2039Regla del modus tollens\u203a\n\ntext \u2039Ejemplo 19 (p. 20) Demostrar la regla del modus tollens a partir \n  de las reglas b\u00e1sicas.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_20_1:\n  assumes 1: \"F \u27f6 G\" and \n          2: \"\u00acG\" \n  shows \"\u00acF\"\nproof (rule notI)\n  assume 3: \"F\"\n  have 4: \"G\" using 1 3 by (rule mp)\n  show False using 2 4 by (rule notE)\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_20_2:\n  assumes \"F \u27f6 G\"\n          \"\u00acG\" \n  shows   \"\u00acF\"\nproof \n  assume \"F\"\n  with assms(1) have \"G\" ..\n  with assms(2) show False ..\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_20_3:\n  assumes \"F \u27f6 G\"\n          \"\u00acG\" \n  shows \"\u00acF\"\n  using assms\n  by simp \n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_20_4: \n  \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"  \n  apply (rule notI)\n  apply (drule mp)\n   apply assumption\n  apply (erule notE)\n  apply assumption\n  done\n\nsubsection \u2039Regla de la introducci\u00f3n de la doble negaci\u00f3n\u203a\n\ntext \u2039Ejemplo 21 (p. 21) Demostrar la regla de introducci\u00f3n de la doble\n  negaci\u00f3n a partir de las reglas b\u00e1sicas.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_21_1:\n  assumes 1: \"F\" \n  shows \"\u00ac\u00acF\"\nproof (rule notI)\n  assume 2: \"\u00acF\"\n  show False using 2 1 by (rule notE)\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_21_2:\n  assumes \"F\" \n  shows \"\u00ac\u00acF\"\nproof \n  assume \"\u00acF\"\n  then show False using assms ..\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_21_3:\n  assumes \"F\" \n  shows \"\u00ac\u00acF\"\n  using assms\n  by simp \n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_21_4: \n  \"F \u27f9 \u00ac\u00acF\"  \n  apply (rule notI)\n  apply (erule notE)\n  apply assumption\n  done\n\nsubsection \u2039Regla de reducci\u00f3n al absurdo\u203a\n\ntext \u2039La regla de reducci\u00f3n al absurdo en Isabelle se correponde con la\n  regla cl\u00e1sica de contradicci\u00f3n \n  \u00b7 ccontr: (\u00acP \u27f9 False) \u27f9 P\n\u203a\n\nsubsection \u2039Ley del tercio excluso\u203a\n\ntext \u2039La ley del tercio excluso es \n  \u00b7 excluded_middle: \u00acP \u2228 P\n\u203a\n\ntext \u2039Ejemplo 22 (p. 23). Demostrar la ley del tercio excluso a partir de\n  las reglas b\u00e1sicas.\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_22_1:\n  \"F \u2228 \u00acF\"\nproof (rule ccontr)\n  assume 1: \"\u00ac(F \u2228 \u00acF)\"\n  then show False\n  proof (rule notE)\n    show \"F \u2228 \u00acF\"\n    proof (rule disjI2)\n      show \"\u00acF\"\n      proof (rule notI)\n        assume 2: \"F\"\n        then have 3: \"F \u2228 \u00acF\" by (rule disjI1)\n        show False using 1 3 by (rule notE)\n      qed\n    qed\n  qed\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_22_2:\n  \"F \u2228 \u00acF\"\nproof (rule ccontr)\n  assume \"\u00ac(F \u2228 \u00acF)\"\n  then show False\n  proof (rule notE)\n    show \"F \u2228 \u00acF\"\n    proof (rule disjI2)\n      show \"\u00acF\"\n      proof (rule notI)\n        assume \"F\"\n        then have \"F \u2228 \u00acF\" ..\n        with \u2039\u00ac(F \u2228 \u00acF)\u203ashow False ..\n      qed\n    qed\n  qed\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_22_3:\n  \"F \u2228 \u00acF\"\n  using assms\n  by simp \n\nsubsection \u2039Ejemplo 23\u203a\n\ntext \u2039Ejemplo 23 (p. 24). Demostrar\n     p \u27f6 q \u22a2 \u00acp \u2228 q\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_23_1:\n  assumes 1: \"p \u27f6 q\" \n  shows \"\u00acp \u2228 q\"\nproof -\n  have \"\u00acp \u2228 p\" by (rule excluded_middle)\n  then show \"\u00acp \u2228 q\"\n  proof (rule disjE)\n    { assume \"\u00acp\"\n      then show \"\u00acp \u2228 q\" by (rule disjI1) }\n  next\n    { assume 2: \"p\"\n      have \"q\" using 1 2 by (rule mp)\n      then show \"\u00acp \u2228 q\" by (rule disjI2) }\n  qed\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_23_2:\n  assumes \"p \u27f6 q\" \n  shows \"\u00acp \u2228 q\"\nproof -\n  have \"\u00acp \u2228 p\" ..\n  then show \"\u00acp \u2228 q\"\n  proof \n    { assume \"\u00acp\"\n      then show \"\u00acp \u2228 q\" .. }\n  next\n    { assume \"p\"\n      with assms have \"q\" ..\n      then show \"\u00acp \u2228 q\" .. }\n  qed\nqed    \n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_23_3:\n  assumes \"p \u27f6 q\" \n  shows \"\u00acp \u2228 q\"\n  using assms\n  by simp \n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_23_4: \n  \"p \u27f6 q \u27f9 \u00acp \u2228 q\"\n  apply (cut_tac P=\"p\" in excluded_middle)\n  apply (erule disjE)\n   apply (rule disjI1)\n   prefer 2\n   apply (drule mp)\n    prefer 2\n    apply (rule disjI2)\n    apply assumption+\n  done\n\nsection \u2039Demostraciones por contradicci\u00f3n\u203a\n\nsubsection \u2039Ejemplo 24\u203a\n\ntext \u2039Ejemplo 24. Demostrar que \n     \u00acp, p \u2228 q \u22a2 q\n\u203a\n\nsubsubsection \u2039Demostraci\u00f3n detallada\u203a\n\n\u2015 \u2039La demostraci\u00f3n detallada es\u203a\nlemma ejemplo_24_1:\n  assumes \"\u00acp\"\n          \"p \u2228 q\"\n  shows   \"q\"\nusing \u2039p \u2228 q\u203a\nproof (rule disjE)\n  assume \"p\"\n  with assms(1) show \"q\" by contradiction \nnext\n  assume \"q\"\n  then show \"q\" by assumption\nqed\n\nsubsubsection \u2039Demostraci\u00f3n estructurada\u203a\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ejemplo_24_2:\n  assumes \"\u00acp\"\n          \"p \u2228 q\"\n  shows \"q\"\nusing \u2039p \u2228 q\u203a\nproof \n  assume \"p\"\n  with assms(1) show \"q\" ..\nnext\n  assume \"q\"\n  then show \"q\" .\nqed\n\nsubsubsection \u2039Demostraci\u00f3n autom\u00e1tica\u203a\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ejemplo_24_3:\n  assumes \"\u00acp\"\n          \"p \u2228 q\"\n  shows \"q\"\n  using assms\n  by simp \n\nsubsubsection \u2039Demostraci\u00f3n aplicativa\u203a\n\nlemma ejemplo_24_4: \n  \"\u27e6\u00acp ; p \u2228 q\u27e7 \u27f9 q\"  \n  apply (erule disjE)\n   apply (erule notE)\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\/R7\">7\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 completado 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\/6902"}],"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=6902"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6902\/revisions"}],"predecessor-version":[{"id":6904,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6902\/revisions\/6904"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6902"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6902"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6902"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}