PDF de programación - 2013 Introduccion a la demostracion asistida por ordenador con IsabelleHOL

Introducción a la demostracción asistida

por ordenador con Isabelle/HOL

José A. Alonso Jiménez

Grupo de Lógica Computacional
Dpto. de Ciencias de la Computación e Inteligencia Artificial
Universidad de Sevilla
Sevilla, 16 de agosto de 2013

2

Esta obra está bajo una licencia Reconocimiento–NoComercial–CompartirIgual 2.5 Spain
de Creative Commons.

Se permite:

copiar, distribuir y comunicar públicamente la obra

hacer obras derivadas

Bajo las condiciones siguientes:

Reconocimiento. Debe reconocer los créditos de la obra de la manera especificada
por el autor.

No comercial. No puede utilizar esta obra para fines comerciales.

Compartir bajo la misma licencia. Si altera o transforma esta obra, o genera una
obra derivada, sólo puede distribuir la obra generada bajo una licencia idéntica a
ésta.

Al reutilizar o distribuir la obra, tiene que dejar bien claro los términos de la licencia
de esta obra.

Alguna de estas condiciones puede no aplicarse si se obtiene el permiso del titular
de los derechos de autor.

Esto es un resumen del texto legal (la licencia completa). Para ver una copia de esta
licencia, visite http://creativecommons.org/licenses/by-nc-sa/2.5/es/ o envie una
carta a Creative Commons, 559 Nathan Abbott Way, Stanford, California 94305, USA.

Índice general

I Temas

1. Deducción natural en lógica proposicional

2. Deducción natural en lógica de primer orden

3. Resumen de Isabelle/Isar y de la lógica

4. Programación funcional con Isabelle/HOL

5. Razonamiento sobre programas

6. Razonamiento por casos y por inducción

7. Caso de estudio: Compilación de expresiones

8. Conjuntos, funciones y relaciones

II Ejercicios

1. Deducción natural en lógica proposicional

2. Argumentación lógica proposicional

3. Eliminación de conectivas

4. Deducción natural en lógica de primer orden

5. Argumentación lógica de primer orden

6. Argumentación lógica de primer orden con igualdad

7. Programación funcional con Isabelle/HOL

3

7

9

39

57

61

71

87

105

113

133

135

153

159

161

173

185

191

4

Índice general

8. Razonamiento sobre programas

9. Cons inverso

10. Cuantificadores sobre listas

11. Sustitución, inversión y eliminación

12. Menor posición válida

13. Número de elementos válidos

14. Contador de occurrencias

15. Suma y aplanamiento de listas

16. Conjuntos mediante listas

17. Ordenación de listas por inserción

18. Ordenación de listas por mezcla

19. Recorridos de árboles

20. Plegados de listas y de árboles

21. Árboles binarios completos

22. Diagramas de decisión binarios

23. Representación de fórmulas proposicionales mediante polinomios

Bibliografía

197

203

205

211

217

219

221

225

231

235

241

247

253

261

265

275

282

Introducción

Este libro es una recopilación de los temas y relaciones de ejercicios del curso de
Razonamiento automático1. El curso es una introducción a la demostración asistida por
ordenador con Isabelle/HOL2 y consta de tres niveles.

En el primer nivel se presenta la formalización de las demostraciones por deducción
natural. La presentación se basa en la realizada en los cursos de Lógica informática3 (de
2o del Grado en Informática) y Lógica matemática y fundamentos4 (de 3o del Grado en
Matemáticas), en concreto en los temas de deducción natural proposicional5 y de de
primer orden6 En este nivel se incluye los 3 primeros temas y las 6 primeras relaciones
de ejercicios.

En el segundo nivel se presenta la programación funcional en Isabelle/HOL y el
razonamiento sobre programas. La presentación se basa en la introducción a la progra-
mación con Haskell realizada en los cursos de Informática7 (de 1o del Grado en Mate-
máticas) y Programación declarativa8 (de 3o del Grado en Informática), en concreto en el
tema 89 (para el razonamiento sobre programas) y en los restantes 9 primeros temas. En
este nivel se incluye los temas 4, 5 y 6 y las relaciones de ejercicios desde la 7 a la 21.

En el tercer nivel se presentan casos de estudios y extensiones de la lógica para tra-
bajar con conjuntos, relaciones y funciones. En este nivel se incluye los temas y y 8 y las
relaciones de ejercicios 22 y 23.

Tanto los temas como las relaciones de ejercicios se presentan como teorías de Isabe-
lle/HOL (versión Isabelle2013). Conforme se necesitan se va comentando los elementos
del Isabelle/HOL.

De Isabelle2013 se dispone se dispone de versiones libres para Linux, Windows y

Mac OS X. Para instalarlo basta seguir la guía de instalación10.

1http://www.cs.us.es/~jalonso/cursos/m-ra-12
2http://www.cl.cam.ac.uk/research/hvg/Isabelle
3http://www.cs.us.es/~jalonso/cursos/li-12
4http://www.cs.us.es/~jalonso/cursos/lmf-12
5http://www.cs.us.es/~jalonso/cursos/li-12/temas/tema-2.pdf
6http://www.cs.us.es/~jalonso/cursos/li-12/temas/tema-8.pdf
7http://www.cs.us.es/~jalonso/cursos/i1m-12
8http://www.cs.us.es/cursos/pd-2012
9http://www.cs.us.es/~jalonso/cursos/i1m-12/temas/tema-8t.pdf
10http://www.cl.cam.ac.uk/research/hvg/Isabelle/installation.html

5

6

Índice general

Parte I

Temas

7

Tema 1

Deducción natural en lógica
proposicional

header {* Tema 1: Deducción natural proposicional con Isabelle/HOL *}

theory T1_Deduccion_natural_en_logica_proposicional
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 de "Lógica informática" (LI)
http://goo.gl/AwDiv

La página al lado de cada ejemplo indica la página de las transparencias
de LI 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:

9

10

Tema 1. Deducción natural en lógica proposicional

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:
· conjunct1:
· conjunct2:

[|P; Q|] =⇒ P ∧ Q
P ∧ Q =⇒ P
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

Razonamiento automático (2012–13)

11

· ".." 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"
"q ∧ r"

shows
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"
"q ∧ r"

shows

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

text {*

12

Tema 1. Deducción natural en lógica proposicional

Nota sobre el lenguaje: En la demostración anterior se ha usado
· "[| ... |]" para representar las hipótesis,
· ";" para separar las hipótesis y
· "=⇒" para separar las hipótesis de la conclusión. *}

text {* Se puede hacer la demostración por razonamiento hacia atrás,

como sigue *}

lemma ejemplo_1_6:
assumes "p ∧ q"
"q ∧ r"
proof (rule conjI)

and "r"

shows

show "q" using assms(1) by (rule conjunct2)

next

show "r" using assms(2) by this

qed

text {*

regla r,

Nota sobre el lenguaje: En la demostración anterior se ha usado
· "proof (rule r)" para indicar que se hará la demostración con la
· "next" para indicar el comienzo de la prueba del siguiente
· "this" para indicar el hecho actual. *}

subobjetivo,

text {* Se pueden dejar implícitas las reglas como sigue *}

lemma ejemplo_1_7:
assumes "p ∧ q"
"r"
"q ∧ r"

shows

proof

show "q" using assms(1) ..

next

show "r" using assms(2) .

qed

text {*

Nota sobre el lenguaje: En la demostración anterior se ha usado

Razonamiento automático (2012–13)

13

· "." para indicar por el hecho actual. *}

subsection {* Reglas de la doble negación *}

text {*

La regla de eliminación de la doble negación es
· notnotD: ¬¬ P =⇒ P

Para ajustarnos al tema de LI vamos a introducir la siguiente regla de
introducción de la doble negación
· notnotI: P =⇒ ¬¬ P
aunque, de momento, no detallamos su demostración.

*}
lemma notnotI [intro!]: "P =⇒ ¬¬ P"
by auto

text {*

Ejemplo 2. (p. 5)

p, ¬¬(q ∧ r) ¬¬p ∧ r

*}

-- "La demostración detallada es"
lemma ejemplo_2_1:

assumes 1: "p" and

2: "¬¬(q ∧ r)"

"¬¬p ∧ r"

shows
proof -
have 3: "¬¬p" using 1 by (rule notnotI)
have 4: "q ∧ r" using 2 by (rule notnotD)
have 5: "r" using 4 by (rule conjunct2)
show 6: "¬¬p ∧ r" using 3 5 by (rule conjI)

qed

-- "La demostración estructurada es"
lemma ejemplo_2_2:

assumes "p"

"¬¬(q ∧ r)"
"¬¬p ∧ r"

shows
proof -

14

Tema 1. Deducción natural en lógica proposicional

"¬¬p" using assms(1) ..
"q ∧ r" using assms(2) by (rule notnotD)

have
have
hence "r" ..
with `¬¬