LMF2017: Deducción natural proposicional (2)
En la segunda parte de la clase de hoy del curso Lógica matemática y fundamentos se ha continuado el estudio de la deducción natural en la lógica proposicional.
Se han estudiado las siguientes reglas básicas
- Regla de copia
- Reglas de la negación
- Reglas del bicondicional
y la siguientes reglas derivadas:
- Regla del modus tollens
- Regla de introducción de doble negación
- Regla de reducción al absurdo
- Ley del tercio excluido
Finalmente, se ha comentado la instalación de Isabelle y su uso para demostrar una fórmula con distinto nivel de detalle.
Las transparencias de esta clase son las 12-29 del tema 2 y la teoría Isabelle es
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 |
header {* Tema 2: Deducción natural proposicional con Isabelle/HOL *} theory T2 imports Main begin text {* En este tema se presentan los ejemplos del tema de deducción natural proposicional siguiendo la presentación de Huth y Ryan en su libro "Logic in Computer Science" http://goo.gl/qsVpY y, más concretamente, a la forma como se explica en la asignatura. La página al lado de cada ejemplo indica la página de las transparencias donde se encuentra la demostración. *} subsection {* Reglas de la conjunción *} text {* Ejemplo 1 (p. 4). Demostrar que p ∧ q, r ⊢ q ∧ r. *} -- "La demostración detallada es" lemma ejemplo_1_1: assumes 1: "p ∧ q" and 2: "r" shows "q ∧ r" proof - have 3: "q" using 1 by (rule conjunct2) show 4: "q ∧ r" using 3 2 by (rule conjI) qed thm ejemplo_1_1 text {* Notas sobre el lenguaje: En la demostración anterior se ha usado · "assumes" para indicar las hipótesis, · "and" para separar las hipótesis, · "shows" para indicar la conclusión, · "proof" para iniciar la prueba, · "qed" para terminar la pruebas, · "-" (después de "proof") para no usar el método por defecto, · "have" para establecer un paso, · "using" para usar hechos en un paso, · "by (rule ..)" para indicar la regla con la que se peueba un hecho, · "show" para establecer la conclusión. Notas sobre la lógica: Las reglas de la conjunción son · conjI: ⟦P; Q⟧ ⟹ P ∧ Q · conjunct1: P ∧ Q ⟹ P · conjunct2: P ∧ Q ⟹ Q *} text {* Se pueden dejar implícitas las reglas como sigue *} lemma ejemplo_1_2: assumes 1: "p ∧ q" and 2: "r" shows "q ∧ r" proof - have 3: "q" using 1 .. show 4: "q ∧ r" using 3 2 .. qed text {* Nota sobre el lenguaje: En la demostración anterior se ha usado · ".." para indicar que se prueba por la regla correspondiente. *} text {* Se pueden eliminar las etiquetas como sigue *} lemma ejemplo_1_3: assumes "p ∧ q" "r" shows "q ∧ r" proof - have "q" using assms(1) .. thus "q ∧ r" using assms(2) .. qed text {* Nota sobre el lenguaje: En la demostración anterior se ha usado · "assms(n)" para indicar la hipótesis n y · "thus" para demostrar la conclusión usando el hecho anterior. Además, no es necesario usar and entre las hipótesis. *} text {* Se puede automatizar la demostración como sigue *} lemma ejemplo_1_4: assumes "p ∧ q" "r" shows "q ∧ r" using assms by auto text {* Nota sobre el lenguaje: En la demostración anterior se ha usado · "assms" para indicar las hipótesis y · "by auto" para demostrar la conclusión automáticamente. *} text {* Se puede automatizar totalmente la demostración como sigue *} lemma ejemplo_1_5: "⟦p ∧ q; r⟧ ⟹ q ∧ r" by auto end |