PDF de programación - Teoría computacional (en ACL2) sobre cálculos proposicionales

Universidad de Sevilla

Departamento de Ciencias de la Computación

e Inteligencia Artificial

Teoría computacional (en ACL2)

sobre cálculos proposicionales

Memoria presentada por
Francisco Jesús Martín Mateos
para optar al grado de
Doctor en Matemáticas
por la Universidad de Sevilla

V. B. Director

Francisco Jesús Martín Mateos

D. José Antonio Alonso Jiménez

Sevilla, Junio de 2002

A mis padres ...

... a mis hermanos ...

... y sobre todo, a Inma.

Agradecimientos

El trabajo desarrollado en esta memoria está parcialmente financiado por los
proyectos TIC2000-1368-C03-02 del Ministerio de Ciencia y Tecnología y PB96-
1345 del Ministerio de Educación y Ciencia.

En primer lugar, quiero agradecer a José Antonio Alonso Jiménez su dirección,

apoyo y comprensión, sin los cuáles este trabajo no habría sido posible.

Al Grupo de Lógica Computacional de la Universidad de Sevilla, cuyas reunio-
nes de trabajo han sido fuente de ideas. En especial me gustaría dar las gracias a
José Luis Ruiz Reina por su ayuda incondicional y a María José Hidalgo Doblado
por sus palabras de ánimo.

A los miembros del Departamento de Ciencias de la Computación e Inteligen-
cia Artificial de la Universidad de Sevilla, por lo mucho que me aprecian y me
aguantan.

A J Moore y Matt Kaufmann, creadores del sistema ACL2, por aceptar con
agrado cualquier comentario o sugerencia acerca del sistema y por permitirme
incluir una copia del mismo junto con la memoria.

A mi familia, en especial a mis padres, Asunción y Manuel, que hace mucho

tiempo depositaron su confianza en mi.

Y finalmente a Inma, que siempre está dispuesta a escucharme y animarme.

Sin su apoyo, esta memoria no se habría terminado.

Índice General

1 Introducción

2 El sistema de razonamiento ACL2

2.1 El lenguaje
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2 La lógica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2.1 Ordinales
2.2.2 Relaciones bien fundamentadas
. . . . . . . . . . . . . . .
2.2.3 Principio de definición . . . . . . . . . . . . . . . . . . . .
2.2.4 Principio de inducción . . . . . . . . . . . . . . . . . . . .
2.2.5 Encapsulados . . . . . . . . . . . . . . . . . . . . . . . . .
Instanciación funcional . . . . . . . . . . . . . . . . . . . .
2.2.6
2.2.7 Equivalencias y Congruencias
. . . . . . . . . . . . . . . .
2.3 El demostrador . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3 Un modelo formal de la lógica proposicional

3.1 Sintaxis

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Símbolos y conectivas . . . . . . . . . . . . . . . . . . . . .
3.1.1
3.1.2 Representación de las fórmulas
. . . . . . . . . . . . . . .
3.1.3 Fórmulas proposicionales . . . . . . . . . . . . . . . . . . .
3.1.4 Clasificación de las fórmulas . . . . . . . . . . . . . . . . .
3.1.5 Teorema de descomposición única . . . . . . . . . . . . . .
3.1.6
Símbolos proposicionales de una fórmula . . . . . . . . . .
3.2 Semántica clásica . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.2.1 Asignaciones . . . . . . . . . . . . . . . . . . . . . . . . . .
3.2.2 Funciones de verdad . . . . . . . . . . . . . . . . . . . . .
3.2.3 Valor de una fórmula en una asignación . . . . . . . . . . .
3.2.4
. . . . . . .
3.3 Semántica de Kleene . . . . . . . . . . . . . . . . . . . . . . . . .
3.3.1 K-asignaciones
. . . . . . . . . . . . . . . . . . . . . . . .
3.3.2 Funciones de verdad en K . . . . . . . . . . . . . . . . . .
3.3.3 Valor de una fórmula en una K-asignación . . . . . . . . .
Satisfacibilidad, validez y consecuencia lógica en K . . . .
3.3.4
3.4 Tablas de verdad . . . . . . . . . . . . . . . . . . . . . . . . . . .

Satisfacibilidad, validez y consecuencia lógica

1

19
21
22
24
25
26
27
29
30
31
32

35
35
36
37
39
42
43
44
45
46
48
49
50
54
54
56
57
58
60

i

ii

Índice General

3.4.1 Asignaciones relevantes de una fórmula . . . . . . . . . . .
3.4.2 Decisión de validez basada en tablas de verdad . . . . . . .
3.4.3 Decisión de satisfacibilidad basada en tablas de verdad . .
3.4.4 Tablas de verdad en K . . . . . . . . . . . . . . . . . . . .
3.5 Ejemplos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

4 Cálculo de tableros semánticos

4.1 Notación uniforme

. . . . . . . . . . . . . . . . . . . . . . . . . .
4.1.1 Clasificación basada en la notación uniforme . . . . . . . .
4.1.2 Medida asociada a la notación uniforme
. . . . . . . . . .
4.1.3 Notación uniforme en K . . . . . . . . . . . . . . . . . . .
4.2 Tableros semánticos . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2.1 Tableros semánticos proposicionales . . . . . . . . . . . . .
4.2.2 Modelo de una rama: M ODR . . . . . . . . . . . . . . . .
4.2.3 Corrección y completitud de M ODR . . . . . . . . . . . .
4.2.4
. . . . . . . . . . . . .
4.2.5 Demostrabilidad por tableros: DATT
. . . . . . . . . . . .
. . . . . . . . . . .
4.2.6 Deducibilidad por tableros: DEDU CT
4.2.7 Tableros semánticos en K . . . . . . . . . . . . . . . . . .
4.3 Ejemplos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Satisfacibilidad por tableros: SATT

61
63
65
66
69

73
73
74
78
79
79
80
87
89
91
92
93
95
99

5 Cálculo de secuentes

5.1 Secuentes

103
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
5.1.1 El cálculo G
. . . . . . . . . . . . . . . . . . . . . . . . . 104
. . . . . 110
5.1.2 Contramodelo de un secuente: CON T RAM ODS
. . . . . . 115
5.1.3 Corrección y completitud de CON T RAM ODS
. . . . . . . . . . . 116
5.1.4 Demostrabilidad por secuentes: DATS
5.1.5
. . . . . . . . . . . . 117
5.1.6 Deducibilidad por secuentes: DEDU CS . . . . . . . . . . . 119
Secuentes en K . . . . . . . . . . . . . . . . . . . . . . . . 120
5.1.7
5.2 Ejemplos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125

Satisfacibilidad por secuentes: SATS

6 Extensiones de ACL2

6.1 Pruebas de terminación basadas en multiconjuntos

129
. . . . . . . . 130
6.1.1 Relaciones bien fundamentadas entre multiconjuntos
. . . 131
6.1.2 El comando defmul . . . . . . . . . . . . . . . . . . . . . . 139
6.1.3 Ejemplo . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140
. . . . . . . . . . . . . . . . . . . . . . . . . . . 144
6.2.1 Teorías genéricas en ACL2 . . . . . . . . . . . . . . . . . . 144
6.2.2 Herramienta de instanciación genérica
. . . . . . . . . . . 147
6.2.3 Ejemplo . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151

6.2 Teorías genéricas

Índice General

iii

7 Sistemas de transformación proposicionales

155
7.1 Un marco genérico para la decisión de satisfacibilidad . . . . . . . 156
7.1.1 Un algoritmo genérico de decisión de satisfacibilidad: SATG 156
7.1.2 Terminación de SATG . . . . . . . . . . . . . . . . . . . . . 162
7.1.3 Corrección y completitud de SATG
. . . . . . . . . . . . . 163
7.1.4 Un algoritmo genérico de decisión de validez: DATG . . . . 165
7.1.5 La teoría genérica *sat-generico* . . . . . . . . . . . . . 165
Sistemas de transformación proposicionales en K . . . . . . 166
7.1.6
7.2 Un STP exitoso basado en tableros semánticos . . . . . . . . . . . 168
7.2.1 Descripción del STP exitoso T . . . . . . . . . . . . . . . . 168
7.2.2 Formalización de T . . . . . . . . . . . . . . . . . . . . . . 170
7.2.3 Un K-STP exitoso basado en tableros semánticos
. . . . . 176
. . . . . . . . . . . . . . . . 176
7.3.1 Descripción del STP exitoso S . . . . . . . . . . . . . . . . 177
7.3.2 Formalización de S . . . . . . . . . . . . . . . . . . . . . . 179
7.3.3 Un K-STP exitoso basado en secuentes . . . . . . . . . . . 184
7.4 Ejemplos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185

7.3 Un STP exitoso basado en secuentes

8 Procedimiento de Davis y Putnam

189
8.1 Cláusulas y formas clausales . . . . . . . . . . . . . . . . . . . . . 190
Sintaxis y semántica . . . . . . . . . . . . . . . . . . . . . 190
8.1.1
8.1.2 Transformación a forma clausal: FC . . . . . . . . . . . . 195
8.1.3 Cláusulas y formas clausales en K . . . . . . . . . . . . . . 203
8.2 Davis y Putnam . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205
8.2.1 Transformaciones de formas clausales . . . . . . . . . . . . 206
8.2.2 Decisión de satisfacibilidad por bifurcación: SATB . . . . . 215
8.2.3 Decisión de satisfacibilidad por Davis-Putnam: SATD . . . 220
8.2.4 Procedimiento de Davis y Putnam en K . . . . . . . . . . 225
8.3 Un STP exitoso basado en Davis-Putnam . . . . . . . . . . . . . . 227
8.3.1 Descripción del STP exitoso D
. . . . . . . . . . . . . . . 228
8.3.2 Formalización de D
. . . . . . . . . . . . . . . . . . . . . 230
8.4 Ejemplos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 236

9 Resolución

241
9.1 Resolución condicionada . . . . . . . . . . . . . . . . . . . . . . . 242
9.1.1 Conjuntos saturados por resolución condicionada . . . . . 242
9.1.2 Decisión de insatisfacibilidad por saturación: IN SATR . . 248
9.1.3 Terminación de IN SATR . . . . . . . . . . . . . . . . . . . 252
9.1.4 Corrección de IN SATR y otras propiedades
. . . . . . . . 255
9.2 Teorema de completitud de Bezem . . . . . . . . . . . . . . . . . 258
9.2.1 Conjuntos representantes . . . . . . . . . . . . . . . . . . . 259
9.2.2 Modelo de un conjunto saturado por resolución . . . . . . 263
9.2.3 Completitud de IN SATR . . . . . . . . . . . . . . . . . . 271

iv

Índice General

9.3 Teoría genérica e instancias

. . . . . . . . . . . . . . . . . . . . . 272
9.3.1 La teoría genérica *resolucion* . . . . . . . . . . . . . . 272
9.3.2
Instancias . . . . . . . . . . . . . . . . . . . . . . . . . . . 272
9.4 Ejemplos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 282

10 Conclusiones

Bibliografía

Glosario

285

297

298

Capítulo 1

Introducción

Uno de los primeros objetivos de la Inteligencia Artificial,