LMF2017 – Página 5

LMF2017: Deducción natural proposicional (2)

PorJosé A. Alonso 21 febrero 201723 febrero 2017

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

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

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

LMF2017: Lógica y programación

PorJosé A. Alonso 21 febrero 201723 febrero 2017

En la primera parte de la clase de hoy del curso Lógica matemática y fundamentos se han comentado algunas relaciones entre la lógica y la programación.

En primer lugar, a partir del artículo The Curry-Howard correspondence between programs and proofs se han comentado cómo los tipos se corresponden con las fórmulas y la existencia de funciones de un tipo dado se corresponde con la veracidad de su fórmula.

Como lectura complementario se ha recomendado el artículo El isomorfismo de Curry-Howard y una introducción a Coq.

Para analizar la distancia del lenguaje matemático a los de programación, se ha comentado el artículo From math to machine: translating a function to machine code que partiendo de la definición matemática del factorial expica su representación en un lenguaje funcional (Haskell), en uno imperativo (C), en ensamblador y en código máquina.

LMF2017: Sintaxis de la lógica proposicional y representación del conocimiento

PorJosé A. Alonso 15 febrero 2017

En la primera parte de la clase de hoy del curso Lógica matemática y fundamentos se han comentados las soluciones propuestas de la 1ª relación de ejercicios sobre sintaxis de la lógica proposicional y representación del conocimiento.

En la segunda parte, se ha explicado cómo hacer demostraciones por deducción natural usando Pandora. Su uso se muestra en este vídeo.

Finalmente, se ha propuesto la 2ª relación de ejercicios.

LMF2017: Deducción natural proposicional (1)

PorJosé A. Alonso 14 febrero 201715 febrero 2017

En la segunda parte de la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la deducción natural en la lógica proposicional.

Se ha comenzado repasando las cuestiones fundamentales estudiadas en el tema 1:

¿Qué es una fórmula?
¿Qué significa que una fórmula sea verdadera?

y planteando una nueva cuestión

¿Qué es un teorema?

para responderla, de forma análoga al uso de modelos para responder a la 2ª cuestión, se comenta el uso de las demostraciones.

El primer método de demostración que se presenta es el de deducción natural. Se han estudiado las siguientes reglas:

Reglas de la conjunción
Reglas de la doble negación
Regla de eliminación del condicional
Regla derivada de modus tollens (MT)
Regla de introducción del condicional
Reglas de la disyunción

Las transparencias de esta clase son las 1-12 del tema 2.

LMF2017: Sintaxis y semántica de la lógica proposicional (2)

PorJosé A. Alonso 14 febrero 201715 febrero 2017

En la primera parte de la clase de hoy del curso Lógica matemática y fundamentos se ha continuado el estudio de la semántica de la lógica proposicional.

Se ha demostrado la equivalencia de los siguientes problemas

decidir si una fórmula es consecuencia lógica de un conjunto finito de fórmulas,
decidir si una fórmula es una tautología,
decidir si una fórmula es insatisfacible y
decidir si un conjunto de fórmulas es inconsistente.

Como aplicación se ha visto la decisión de la corrección de un argumento y la resolución de rompecabezas lógicos. En la solución del rompecabezas se ha explicado el uso del Gateway to Logic.

Las transparencias de esta clase son las páginas 30-34 del tema 1.