matematicas discretas
Páginas: 12 (2946 palabras)
Publicado: 11 de septiembre de 2014
La Lógica Computacional ACL2
Programación y Razonamiento
Automático
I. Medina Bulo
F. Palomo Lozano*
{inmaculada.medina,francisco.palomo}@uca.es
Departamento de Lenguajes y Sistemas Informáticos
Universidad de Cádiz
Índice
1. Introducción
4
2. Las tres visiones de ACL2
4
2.1. ACL2 es un lenguaje de programación aplicativo . . . . . . .
5
2.1.1. Tipos de datos . .. . . . . . . . . . . . . . . . . . . .
6
2.1.2. Expresiones . . . . . . . . . . . . . . . . . . . . . . . .
9
2.1.3. Funciones y macros
10
2.2. ACL2 es una Lógica Computacional . . . . . . . . . . . . . .
15
2.2.1. Lógica de primer orden sin cuantificadores . . . . . . .
17
2.2.2. Axiomas y reglas de inferencia . . . . . . . . . . . . .
19
2.2.3. Principios deextensión y de inducción . . . . . . . . .
23
2.2.4. Otras características . . . . . . . . . . . . . . . . . . .
*
. . . . . . . . . . . . . . . . . . .
25
Escuela Superior de Ingeniería de Cádiz. C/ Chile, s/n. 11003 Cádiz. España.
1
c I. Medina Bulo, F. Palomo Lozano
Cádiz, 2012
2.3. ACL2 es un sistema de razonamiento automático . . . . . . .
26
2.3.1. Órdenesbásicas de demostración . . . . . . . . . . . .
27
2.3.2. Características del demostrador . . . . . . . . . . . . .
29
2.3.3. Técnicas de demostración . . . . . . . . . . . . . . . .
30
3. Una aplicación práctica
34
3.1. Operaciones en listas ordenadas . . . . . . . . . . . . . . . . .
35
3.1.1. Definiciones y su admisión . . . . . . . . . . . . . . . .
35
3.1.2.Propiedades y su demostración automática . . . . . .
36
3.1.3. Verificación de protecciones . . . . . . . . . . . . . . .
38
3.2. Razonamiento por composición . . . . . . . . . . . . . . . . .
39
3.3. Operaciones sobre listas ordenadas genéricas . . . . . . . . . .
41
3.3.1. El problema del orden . . . . . . . . . . . . . . . . . .
41
3.3.2. Abstracción de las nocionesde orden y equivalencia .
43
3.3.3. Operaciones genéricas, equivalencia y congruencias . .
46
3.4. Propiedades de las operaciones genéricas . . . . . . . . . . . .
48
3.5. Instanciación de las operaciones y sus propiedades . . . . . .
48
3.6. Conclusiones . . . . . . . . . . . . . . . . . . . . . . . . . . .
50
2
c I. Medina Bulo, F. Palomo Lozano
Cádiz, 2012Tablas
1.
Constantes numéricas. . . . . . . . . . . . . . . . . . . . . . .
7
2.
Listas homogéneas. . . . . . . . . . . . . . . . . . . . . . . . .
9
3.
Algunas funciones y macros primitivas. . . . . . . . . . . . . .
11
4.
Símbolos lógicos y su representación. . . . . . . . . . . . . . .
18
5.
Operadores derivados. . . . . . . . . . . . . . . . . . . . .. .
20
6.
Ordinales y su representación. . . . . . . . . . . . . . . . . . .
24
7.
Consejos habituales. . . . . . . . . . . . . . . . . . . . . . . .
28
8.
Clases de regla más comunes. . . . . . . . . . . . . . . . . . .
28
Figuras
1.
Procesos del demostrador de teoremas. . . . . . . . . . . . . .
3
31
c I. Medina Bulo, F. Palomo Lozano
1.Cádiz, 2012
Introducción
Dentro del amplio espectro de sistemas de razonamiento automático, existen
varios especialmente adecuados para la especificación y verificación formal
de sistemas informáticos.
Uno de ellos, ACL2, merece especial atención ya que formaliza un subconjunto de un lenguaje de programación real y con él se han obtenido grandes
éxitos en la verificación formal automatizada tantode sistemas de hardware como de software, además de en la demostración por computador de
conocidos teoremas de la Lógica y de las Matemáticas.
Se expondrá a continuación una descripción de ACL2 atendiendo a los diferentes puntos de vista desde los que puede observarse. El lector debe advertir
que esta descripción no es exhaustiva y, de hecho, en algunos puntos supone
una simplificación de...
Programación y Razonamiento
Automático
I. Medina Bulo
F. Palomo Lozano*
{inmaculada.medina,francisco.palomo}@uca.es
Departamento de Lenguajes y Sistemas Informáticos
Universidad de Cádiz
Índice
1. Introducción
4
2. Las tres visiones de ACL2
4
2.1. ACL2 es un lenguaje de programación aplicativo . . . . . . .
5
2.1.1. Tipos de datos . .. . . . . . . . . . . . . . . . . . . .
6
2.1.2. Expresiones . . . . . . . . . . . . . . . . . . . . . . . .
9
2.1.3. Funciones y macros
10
2.2. ACL2 es una Lógica Computacional . . . . . . . . . . . . . .
15
2.2.1. Lógica de primer orden sin cuantificadores . . . . . . .
17
2.2.2. Axiomas y reglas de inferencia . . . . . . . . . . . . .
19
2.2.3. Principios deextensión y de inducción . . . . . . . . .
23
2.2.4. Otras características . . . . . . . . . . . . . . . . . . .
*
. . . . . . . . . . . . . . . . . . .
25
Escuela Superior de Ingeniería de Cádiz. C/ Chile, s/n. 11003 Cádiz. España.
1
c I. Medina Bulo, F. Palomo Lozano
Cádiz, 2012
2.3. ACL2 es un sistema de razonamiento automático . . . . . . .
26
2.3.1. Órdenesbásicas de demostración . . . . . . . . . . . .
27
2.3.2. Características del demostrador . . . . . . . . . . . . .
29
2.3.3. Técnicas de demostración . . . . . . . . . . . . . . . .
30
3. Una aplicación práctica
34
3.1. Operaciones en listas ordenadas . . . . . . . . . . . . . . . . .
35
3.1.1. Definiciones y su admisión . . . . . . . . . . . . . . . .
35
3.1.2.Propiedades y su demostración automática . . . . . .
36
3.1.3. Verificación de protecciones . . . . . . . . . . . . . . .
38
3.2. Razonamiento por composición . . . . . . . . . . . . . . . . .
39
3.3. Operaciones sobre listas ordenadas genéricas . . . . . . . . . .
41
3.3.1. El problema del orden . . . . . . . . . . . . . . . . . .
41
3.3.2. Abstracción de las nocionesde orden y equivalencia .
43
3.3.3. Operaciones genéricas, equivalencia y congruencias . .
46
3.4. Propiedades de las operaciones genéricas . . . . . . . . . . . .
48
3.5. Instanciación de las operaciones y sus propiedades . . . . . .
48
3.6. Conclusiones . . . . . . . . . . . . . . . . . . . . . . . . . . .
50
2
c I. Medina Bulo, F. Palomo Lozano
Cádiz, 2012Tablas
1.
Constantes numéricas. . . . . . . . . . . . . . . . . . . . . . .
7
2.
Listas homogéneas. . . . . . . . . . . . . . . . . . . . . . . . .
9
3.
Algunas funciones y macros primitivas. . . . . . . . . . . . . .
11
4.
Símbolos lógicos y su representación. . . . . . . . . . . . . . .
18
5.
Operadores derivados. . . . . . . . . . . . . . . . . . . . .. .
20
6.
Ordinales y su representación. . . . . . . . . . . . . . . . . . .
24
7.
Consejos habituales. . . . . . . . . . . . . . . . . . . . . . . .
28
8.
Clases de regla más comunes. . . . . . . . . . . . . . . . . . .
28
Figuras
1.
Procesos del demostrador de teoremas. . . . . . . . . . . . . .
3
31
c I. Medina Bulo, F. Palomo Lozano
1.Cádiz, 2012
Introducción
Dentro del amplio espectro de sistemas de razonamiento automático, existen
varios especialmente adecuados para la especificación y verificación formal
de sistemas informáticos.
Uno de ellos, ACL2, merece especial atención ya que formaliza un subconjunto de un lenguaje de programación real y con él se han obtenido grandes
éxitos en la verificación formal automatizada tantode sistemas de hardware como de software, además de en la demostración por computador de
conocidos teoremas de la Lógica y de las Matemáticas.
Se expondrá a continuación una descripción de ACL2 atendiendo a los diferentes puntos de vista desde los que puede observarse. El lector debe advertir
que esta descripción no es exhaustiva y, de hecho, en algunos puntos supone
una simplificación de...
Leer documento completo
Regístrate para leer el documento completo.