21 febrero 2017 – Vestigium

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.