{"id":3125,"date":"2013-03-15T16:05:37","date_gmt":"2013-03-15T16:05:37","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3125"},"modified":"2013-03-15T16:05:37","modified_gmt":"2013-03-15T16:05:37","slug":"lmf2013-ejercicios-de-deduccion-natural-en-logica-proposicional-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-ejercicios-de-deduccion-natural-en-logica-proposicional-con-isabellehol\/","title":{"rendered":"LMF2013: Ejercicios de deducci\u00f3n natural en l\u00f3gica proposicional con Isabelle\/HOL"},"content":{"rendered":"<p>En las clases del mi\u00e9rcoles y de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-12\">L\u00f3gica matem\u00e1tica y fundamentos<\/a>  se han comentado soluciones de los ejercicios de deducci\u00f3n natural en l\u00f3gica proposicional con Isabelle\/HOL.<\/p>\n<p>Para cada uno de los ejercicios se ha presentado distintas demostraciones: desde la detallada (que sea parecida a la mostrada en las transparencias) hasta la autom\u00e1tica.<\/p>\n<p>La teor\u00eda con la relaci\u00f3n de ejercicios es<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\r\nheader {* R2: Deducci\u00f3n natural proposicional *}\r\n\r\ntheory R2\r\nimports Main \r\nbegin\r\n\r\ntext {*\r\n  --------------------------------------------------------------------- \r\n  El objetivo de esta relaci\u00f3n es demostrar cada uno de los ejercicios\r\n  usando s\u00f3lo las reglas b\u00e1sicas de deducci\u00f3n natural de la l\u00f3gica\r\n  proposicional (sin usar el m\u00e9todo auto).\r\n\r\n  Las reglas b\u00e1sicas de la deducci\u00f3n natural son las siguientes:\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  \u00b7 notnotD:    \u00ac\u00ac P \u27f9 P\r\n  \u00b7 notnotI:    P \u27f9 \u00ac\u00ac P\r\n  \u00b7 mp:         \u27e6P \u27f6 Q; P\u27e7 \u27f9 Q \r\n  \u00b7 mt:         \u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF \r\n  \u00b7 impI:       (P \u27f9 Q) \u27f9 P \u27f6 Q\r\n  \u00b7 disjI1:     P \u27f9 P \u2228 Q\r\n  \u00b7 disjI2:     Q \u27f9 P \u2228 Q\r\n  \u00b7 disjE:      \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R \r\n  \u00b7 FalseE:     False \u27f9 P\r\n  \u00b7 notE:       \u27e6\u00acP; P\u27e7 \u27f9 R\r\n  \u00b7 notI:       (P \u27f9 False) \u27f9 \u00acP\r\n  \u00b7 iffI:       \u27e6P \u27f9 Q; Q \u27f9 P\u27e7 \u27f9 P = Q\r\n  \u00b7 iffD1:      \u27e6Q = P; Q\u27e7 \u27f9 P \r\n  \u00b7 iffD2:      \u27e6P = Q; Q\u27e7 \u27f9 P\r\n  \u00b7 ccontr:     (\u00acP \u27f9 False) \u27f9 P\r\n  --------------------------------------------------------------------- \r\n*}\r\n\r\ntext {*\r\n  Se usar\u00e1n las reglas notnotI y mt que demostramos a continuaci\u00f3n. *}\r\n\r\nlemma notnotI: \"P \u27f9 \u00ac\u00ac P\"\r\nby auto\r\n\r\nlemma mt: \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"\r\nby auto\r\n\r\nsection {* Implicaciones *}\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 1. Demostrar\r\n       p \u27f6 q, p \u22a2 q\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_1:\r\n  assumes \"p \u27f6 q\"\r\n          \"p\"\r\n  shows \"q\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 2. Demostrar\r\n     p \u27f6 q, q \u27f6 r, p \u22a2 r\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_2:\r\n  assumes \"p \u27f6 q\"\r\n          \"q \u27f6 r\"\r\n          \"p\" \r\n  shows \"r\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 3. Demostrar\r\n     p \u27f6 (q \u27f6 r), p \u27f6 q, p \u22a2 r\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_3:\r\n  assumes \"p \u27f6 (q \u27f6 r)\"\r\n          \"p \u27f6 q\"\r\n          \"p\"\r\n  shows \"r\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 4. Demostrar\r\n     p \u27f6 q, q \u27f6 r \u22a2 p \u27f6 r\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_4:\r\n  assumes \"p \u27f6 q\"\r\n          \"q \u27f6 r\" \r\n  shows \"p \u27f6 r\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 5. Demostrar\r\n     p \u27f6 (q \u27f6 r) \u22a2 q \u27f6 (p \u27f6 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_5:\r\n  assumes \"p \u27f6 (q \u27f6 r)\" \r\n  shows   \"q \u27f6 (p \u27f6 r)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 6. Demostrar\r\n     p \u27f6 (q \u27f6 r) \u22a2 (p \u27f6 q) \u27f6 (p \u27f6 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_6:\r\n  assumes \"p \u27f6 (q \u27f6 r)\" \r\n  shows   \"(p \u27f6 q) \u27f6 (p \u27f6 r)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 7. Demostrar\r\n     p \u22a2 q \u27f6 p\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_7:\r\n  assumes \"p\"  \r\n  shows   \"q \u27f6 p\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 8. Demostrar\r\n     \u22a2 p \u27f6 (q \u27f6 p)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_8:\r\n  \"p \u27f6 (q \u27f6 p)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 9. Demostrar\r\n     p \u27f6 q \u22a2 (q \u27f6 r) \u27f6 (p \u27f6 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_9:\r\n  assumes \"p \u27f6 q\" \r\n  shows   \"(q \u27f6 r) \u27f6 (p \u27f6 r)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 10. Demostrar\r\n     p \u27f6 (q \u27f6 (r \u27f6 s)) \u22a2 r \u27f6 (q \u27f6 (p \u27f6 s))\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_10:\r\n  assumes \"p \u27f6 (q \u27f6 (r \u27f6 s))\" \r\n  shows   \"r \u27f6 (q \u27f6 (p \u27f6 s))\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 11. Demostrar\r\n     \u22a2 (p \u27f6 (q \u27f6 r)) \u27f6 ((p \u27f6 q) \u27f6 (p \u27f6 r))\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_11:\r\n  \"(p \u27f6 (q \u27f6 r)) \u27f6 ((p \u27f6 q) \u27f6 (p \u27f6 r))\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 12. Demostrar\r\n     (p \u27f6 q) \u27f6 r \u22a2 p \u27f6 (q \u27f6 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_12:\r\n  assumes \"(p \u27f6 q) \u27f6 r\" \r\n  shows   \"p \u27f6 (q \u27f6 r)\"\r\noops\r\n\r\nsection {* Conjunciones *}\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 13. Demostrar\r\n     p, q \u22a2  p \u2227 q\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_13:\r\n  assumes \"p\"\r\n          \"q\" \r\n  shows \"p \u2227 q\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 14. Demostrar\r\n     p \u2227 q \u22a2 p\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_14:\r\n  assumes \"p \u2227 q\"  \r\n  shows   \"p\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 15. Demostrar\r\n     p \u2227 q \u22a2 q\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_15:\r\n  assumes \"p \u2227 q\" \r\n  shows   \"q\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 16. Demostrar\r\n     p \u2227 (q \u2227 r) \u22a2 (p \u2227 q) \u2227 r\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_16:\r\n  assumes \"p \u2227 (q \u2227 r)\"\r\n  shows   \"(p \u2227 q) \u2227 r\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 17. Demostrar\r\n     (p \u2227 q) \u2227 r \u22a2 p \u2227 (q \u2227 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_17:\r\n  assumes \"(p \u2227 q) \u2227 r\" \r\n  shows   \"p \u2227 (q \u2227 r)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 18. Demostrar\r\n     p \u2227 q \u22a2 p \u27f6 q\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_18:\r\n  assumes \"p \u2227 q\" \r\n  shows   \"p \u27f6 q\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 19. Demostrar\r\n     (p \u27f6 q) \u2227 (p \u27f6 r) \u22a2 p \u27f6 q \u2227 r   \r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_19:\r\n  assumes \"(p \u27f6 q) \u2227 (p \u27f6 r)\" \r\n  shows   \"p \u27f6 q \u2227 r\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 20. Demostrar\r\n     p \u27f6 q \u2227 r \u22a2 (p \u27f6 q) \u2227 (p \u27f6 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_20:\r\n  assumes \"p \u27f6 q \u2227 r\" \r\n  shows   \"(p \u27f6 q) \u2227 (p \u27f6 r)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 21. Demostrar\r\n     p \u27f6 (q \u27f6 r) \u22a2 p \u2227 q \u27f6 r\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_21:\r\n  assumes \"p \u27f6 (q \u27f6 r)\" \r\n  shows   \"p \u2227 q \u27f6 r\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 22. Demostrar\r\n     p \u2227 q \u27f6 r \u22a2 p \u27f6 (q \u27f6 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_22:\r\n  assumes \"p \u2227 q \u27f6 r\" \r\n  shows   \"p \u27f6 (q \u27f6 r)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 23. Demostrar\r\n     (p \u27f6 q) \u27f6 r \u22a2 p \u2227 q \u27f6 r\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_23:\r\n  assumes \"(p \u27f6 q) \u27f6 r\" \r\n  shows   \"p \u2227 q \u27f6 r\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 24. Demostrar\r\n     p \u2227 (q \u27f6 r) \u22a2 (p \u27f6 q) \u27f6 r\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_24:\r\n  assumes \"p \u2227 (q \u27f6 r)\" \r\n  shows   \"(p \u27f6 q) \u27f6 r\"\r\noops\r\n\r\nsection {* Disyunciones *}\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 25. Demostrar\r\n     p \u22a2 p \u2228 q\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_25:\r\n  assumes \"p\"\r\n  shows   \"p \u2228 q\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 26. Demostrar\r\n     q \u22a2 p \u2228 q\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_26:\r\n  assumes \"q\"\r\n  shows   \"p \u2228 q\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 27. Demostrar\r\n     p \u2228 q \u22a2 q \u2228 p\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_27:\r\n  assumes \"p \u2228 q\"\r\n  shows   \"q \u2228 p\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 28. Demostrar\r\n     q \u27f6 r \u22a2 p \u2228 q \u27f6 p \u2228 r\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_28:\r\n  assumes \"q \u27f6 r\" \r\n  shows   \"p \u2228 q \u27f6 p \u2228 r\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 29. Demostrar\r\n     p \u2228 p \u22a2 p\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_29:\r\n  assumes \"p \u2228 p\"\r\n  shows   \"p\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 30. Demostrar\r\n     p \u22a2 p \u2228 p\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_30:\r\n  assumes \"p\" \r\n  shows   \"p \u2228 p\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 31. Demostrar\r\n     p \u2228 (q \u2228 r) \u22a2 (p \u2228 q) \u2228 r\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_31:\r\n  assumes \"p \u2228 (q \u2228 r)\" \r\n  shows   \"(p \u2228 q) \u2228 r\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 32. Demostrar\r\n     (p \u2228 q) \u2228 r \u22a2 p \u2228 (q \u2228 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_32:\r\n  assumes \"(p \u2228 q) \u2228 r\" \r\n  shows   \"p \u2228 (q \u2228 r)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 33. Demostrar\r\n     p \u2227 (q \u2228 r) \u22a2 (p \u2227 q) \u2228 (p \u2227 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_33:\r\n  assumes \"p \u2227 (q \u2228 r)\" \r\n  shows   \"(p \u2227 q) \u2228 (p \u2227 r)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 34. Demostrar\r\n     (p \u2227 q) \u2228 (p \u2227 r) \u22a2 p \u2227 (q \u2228 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_34:\r\n  assumes \"(p \u2227 q) \u2228 (p \u2227 r)\" \r\n  shows   \"p \u2227 (q \u2228 r)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 35. Demostrar\r\n     p \u2228 (q \u2227 r) \u22a2 (p \u2228 q) \u2227 (p \u2228 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_35:\r\n  assumes \"p \u2228 (q \u2227 r)\" \r\n  shows   \"(p \u2228 q) \u2227 (p \u2228 r)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 36. Demostrar\r\n     (p \u2228 q) \u2227 (p \u2228 r) \u22a2 p \u2228 (q \u2227 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_36:\r\n  assumes \"(p \u2228 q) \u2227 (p \u2228 r)\"\r\n  shows   \"p \u2228 (q \u2227 r)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 37. Demostrar\r\n     (p \u27f6 r) \u2227 (q \u27f6 r) \u22a2 p \u2228 q \u27f6 r\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_37:\r\n  assumes \"(p \u27f6 r) \u2227 (q \u27f6 r)\" \r\n  shows   \"p \u2228 q \u27f6 r\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 38. Demostrar\r\n     p \u2228 q \u27f6 r \u22a2 (p \u27f6 r) \u2227 (q \u27f6 r)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_38:\r\n  assumes \"p \u2228 q \u27f6 r\" \r\n  shows   \"(p \u27f6 r) \u2227 (q \u27f6 r)\"\r\noops\r\n\r\nsection {* Negaciones *}\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 39. Demostrar\r\n     p \u22a2 \u00ac\u00acp\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_39:\r\n  assumes \"p\"\r\n  shows   \"\u00ac\u00acp\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 40. Demostrar\r\n     \u00acp \u22a2 p \u27f6 q\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_40:\r\n  assumes \"\u00acp\" \r\n  shows   \"p \u27f6 q\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 41. Demostrar\r\n     p \u27f6 q \u22a2 \u00acq \u27f6 \u00acp\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_41:\r\n  assumes \"p \u27f6 q\"\r\n  shows   \"\u00acq \u27f6 \u00acp\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 42. Demostrar\r\n     p\u2228q, \u00acq \u22a2 p\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_42:\r\n  assumes \"p\u2228q\"\r\n          \"\u00acq\" \r\n  shows   \"p\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 42. Demostrar\r\n     p \u2228 q, \u00acp \u22a2 q\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_43:\r\n  assumes \"p \u2228 q\"\r\n          \"\u00acp\" \r\n  shows   \"q\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 40. Demostrar\r\n     p \u2228 q \u22a2 \u00ac(\u00acp \u2227 \u00acq)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_44:\r\n  assumes \"p \u2228 q\" \r\n  shows   \"\u00ac(\u00acp \u2227 \u00acq)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 45. Demostrar\r\n     p \u2227 q \u22a2 \u00ac(\u00acp \u2228 \u00acq)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_45:\r\n  assumes \"p \u2227 q\" \r\n  shows   \"\u00ac(\u00acp \u2228 \u00acq)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 46. Demostrar\r\n     \u00ac(p \u2228 q) \u22a2 \u00acp \u2227 \u00acq\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_46:\r\n  assumes \"\u00ac(p \u2228 q)\" \r\n  shows   \"\u00acp \u2227 \u00acq\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 47. Demostrar\r\n     \u00acp \u2227 \u00acq \u22a2 \u00ac(p \u2228 q)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_47:\r\n  assumes \"\u00acp \u2227 \u00acq\" \r\n  shows   \"\u00ac(p \u2228 q)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 48. Demostrar\r\n     \u00acp \u2228 \u00acq \u22a2 \u00ac(p \u2227 q)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_48:\r\n  assumes \"\u00acp \u2228 \u00acq\"\r\n  shows   \"\u00ac(p \u2227 q)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 49. Demostrar\r\n     \u22a2 \u00ac(p \u2227 \u00acp)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_49:\r\n  \"\u00ac(p \u2227 \u00acp)\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 50. Demostrar\r\n     p \u2227 \u00acp \u22a2 q\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_50:\r\n  assumes \"p \u2227 \u00acp\" \r\n  shows   \"q\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 51. Demostrar\r\n     \u00ac\u00acp \u22a2 p\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_51:\r\n  assumes \"\u00ac\u00acp\"\r\n  shows   \"p\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 52. Demostrar\r\n     \u22a2 p \u2228 \u00acp\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_52:\r\n  \"p \u2228 \u00acp\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 53. Demostrar\r\n     \u22a2 ((p \u27f6 q) \u27f6 p) \u27f6 p\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_53:\r\n  \"((p \u27f6 q) \u27f6 p) \u27f6 p\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 54. Demostrar\r\n     \u00acq \u27f6 \u00acp \u22a2 p \u27f6 q\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_54:\r\n  assumes \"\u00acq \u27f6 \u00acp\"\r\n  shows   \"p \u27f6 q\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 55. Demostrar\r\n     \u00ac(\u00acp \u2227 \u00acq) \u22a2 p \u2228 q\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_55:\r\n  assumes \"\u00ac(\u00acp \u2227 \u00acq)\"\r\n  shows   \"p \u2228 q\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 56. Demostrar\r\n     \u00ac(\u00acp \u2228 \u00acq) \u22a2 p \u2227 q\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_56:\r\n  assumes \"\u00ac(\u00acp \u2228 \u00acq)\" \r\n  shows   \"p \u2227 q\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 57. Demostrar\r\n     \u00ac(p \u2227 q) \u22a2 \u00acp \u2228 \u00acq\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_57:\r\n  assumes \"\u00ac(p \u2227 q)\"\r\n  shows   \"\u00acp \u2228 \u00acq\"\r\noops\r\n\r\ntext {* --------------------------------------------------------------- \r\n  Ejercicio 58. Demostrar\r\n     \u22a2 (p \u27f6 q) \u2228 (q \u27f6 p)\r\n  ------------------------------------------------------------------ *}\r\n\r\nlemma ejercicio_58:\r\n  \"(p \u27f6 q) \u2228 (q \u27f6 p)\"\r\noops\r\n\r\nend\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En las clases del mi\u00e9rcoles y de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se han comentado soluciones de los ejercicios de deducci\u00f3n natural en l\u00f3gica proposicional con Isabelle\/HOL. Para cada uno de los ejercicios se ha presentado distintas demostraciones: desde la detallada (que sea parecida a la mostrada en las transparencias) hasta la autom\u00e1tica&#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,202],"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\/3125"}],"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=3125"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3125\/revisions"}],"predecessor-version":[{"id":3126,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3125\/revisions\/3126"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3125"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3125"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3125"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}