Aplicaciones de la Lógica al Desarrollo de Software: Lenguajes Lógicos y Funcionales

Capítulo 1
1.1 Introducción.
1.2 La Máquina de Estados.
1.2.1 Vista Interna del Computador
1.2.2 El Proceso Computacional.
1.2.3 La Máquina de Estados.
1.3 Los Programas del Computador.
1.4 Lenguajes de Programación
1.5 Evolución de los lenguajes de Programación.
1.5.1 Primera Generación: Lenguaje de Máquina.
1.5.2 Segunda Generación: Lenguaje Ensamblador.
1.5.3 Tercera Generación: Lenguajes Procedurales.
1.5.3.1 Independencia de la Máquina.
1.5.3.2 Valores, Tipos, Operadores y Términos.
1.5.3.3 Instrucciones de asignación y de I/O.
1.5.3.4 Instrucciones de Secuenciamiento.
1.5.3.5 Subprogramas y Librerías.
1.5.4 Cuarta Generación: SQL y Lenguajes Declarativos.
1.5.5 Quinta Generación: Uso de la Lógica.
1.6 Resumen del Capítulo.
Capítulo 2
2.1 Introducción
2.2 Paradigma de Instrucciones.
2.3 Paradigma de Funciones (o Procesos).
2.3.1 Especificación de Funciones.
2.3.2 Arquitectura funcional.
2.3.3 Proceso de desarrollo.
2.4 Paradigma de Entidades (o Estructuración de Datos).
2.4.1 Estructuración de los datos en archivos.
2.4.2 Problemas con los Archivos y Aparición de los Gestores de Bases de Datos.
2.4.3 Modelo Relacional.
2.4.4 La especificación formal bajo el modelo Relacional.
2.4.5 Arquitectura Relacional.
2.5 Paradigma de Objetos.
2.5.1 Concepto Clásico de Objeto.
2.5.2 Relaciones entre objetos.
2.5.3 Aplicaciones como Sistemas Dinámicos.
2.5.4 Especificación formal bajo el modelo OO.
2.5.5 Arquitectura Objetual.
2.6 Paradigma de Agentes.
2.7 Resumen del Capítulo.
Capítulo 3
3.1 Introducción
3.2 La Lógica Como una Disciplina de Razonamiento.
3.2.1 Lógica en la antigua Grecia.
3.2.2 La lógica en la matemática moderna.
3.3 La Lógica Como una Disciplina de los Lenguajes.
3.3.1 Sintaxis.
3.3.2 Semántica.
3.3.3 Inferencia.
3.4 Lógica de Proposiciones.
3.4.1 Proposiciones.
3.4.2 Sintaxis de la lógica proposicional.
3.4.2.1 Alfabeto
3.4.2.2 Criterios Formativos
3.4.2.3 Árbol sintáctico
3.4.2.4 Uso de paréntesis.
3.4.2.5 Uso de un orden de precedencia entre los operadores.
3.4.2.6 Uso del sentido de asociatividad entre los operadores.
3.4.3 Semántica.en lógica proposicional.
3.4.3.1 Interpretación.
3.4.3.2 Semántica de los conectores.
3.4.3.3 Semántica de las fbfs complejas.
3.4.3.4 Tipos de fórmulas en relación con las interpretaciones.
3.4.3.5 Semántica de un conjunto de fbfs.
3.4.4 Inferencia en lógica proposicional.
3.4.4.1 Consecuencia lógica y Equivalencia Semántica.
3.4.4.2 Tablas de verdad
3.4.4.3 Criterios demostrativos
3.4.4.3.1 Completitud y consistencia.
3.4.4.3.2 Tautologías como Reglas de Inferencia.
3.4.5 Formas Normales.
3.4.5.1 Substitución de Subfórmulas.
3.4.5.2 Forma Normal Conjuntiva (forma “clausal”).
3.5 Resumen del Capítulo.
3.6 Ejercicios Propuestos.
3.6.1 De la lógica en general
3.6.2 Lógica de Proposiciones
3.6.2.1 ¿Verdadero o falso?.
3.6.2.2 Fórmulas bien y mal formadas
3.6.2.3 Árbol Sintáctico
3.6.2.4 Prueba.
3.6.2.5 Varios
Capítulo 4
4.1 Introducción
4.2 Sintaxis de la lógica de predicados.
4.2.1 Alfabeto de símbolos.
4.2.1.1 Sorts o símbolos de tipo.
4.2.1.2 Términos.
4.2.1.2.1 Constantes
4.2.1.2.2 Variables.
4.2.1.2.3 Términos compuestos.
4.2.1.3 Predicados y plantillas.
4.2.1.3.1 Predicados.
4.2.1.3.2 Plantillas de los predicados y operadores .
4.2.1.4 Cuantificadores.
4.2.2 Criterios Formativos de las fbf en lógica de predicados
4.2.2.1 Criterios formativos de una proposición atómica en lógica de predicados.
4.2.2.2 Uso de cuantificadores.
4.2.2.2.1 Alcance de un cuantificador.
4.2.2.2.2 Ocurrencias de variable.
4.2.2.2.3 Ligaduras de las variables al cuantificador.
4.2.2.3 Uso de conectores
4.3 Semántica en la lógica de Predicados.
4.3.1 Dominio de interpretación.
4.3.2 Significado de las variables.
4.3.3 Extensión de los predicados sobre el dominio.
4.3.4 Valor de verdad de las FBF.
4.3.4.1 Átomos base.
4.3.4.2 Fórmulas Cuantificadas.
4.3.4.3 fbfs complejas
4.3.5 semántica de un conjunto de fbfs.
4.4 Inferencia en lógica de Predicados.
4.4.1 Criterios de demostración propios de la lógica de predicados.
4.4.2 Formas Normales en Lógica de Predicados.
4.4.2.1 Equivalencia Semántica.
4.4.2.2 Forma normal Prenex.
4.5 Tipos de predicados y lógicas asociadas.
4.6 Resumen del Capítulo.
4.7 Ejercicios Propuestos.
4.7.1 Verdadero o falso?
4.7.2 Árboles sintácticos
4.7.3 Variables Libres y Ligadas
4.7.4 Cálculo de valores de verdad.
4.7.5 Varios
Capítulo 5
5.1 Introducción.
5.2 Términos.
5.2.1 Operadores.
5.2.2 Criterios formativos de los términos.
5.2.3 Términos Complejos
5.2.3.1 Árbol Sintáctico.
5.2.3.2 Uso de Paréntesis.
5.2.3.3 Asociatividad y precedencia de operadores.
5.2.4 Semántica de los Operadores.
5.3 Lógica Ecuacional
5.3.1 El predicado de igualdad.
5.3.2 Criterios Demostrativos.
5.3.3 Teoría en lógica ecuacional.
5.3.3.1 Elementos de una teoría en Lógica Ecuacional
5.3.3.1.1 Declaración de sorts.
5.3.3.1.2 Perfil de los operadores.
5.3.3.1.3 Axiomas.
5.3.3.2 Demostración en Lógica Ecuacional.
5.4 Sistemas de Reescritura de Términos (SRT).
5.5 Alcance de los SRTs.
5.6 Especificación en Lógica Ecuacional Multisort.
5.6.1 Signatura Multisort.
5.6.2 Términos.
5.6.3 Ecuaciones.
5.7 SRT
5.7.1 Substitución, Particularización y Emparejamiento.
5.7.2 Ocurrencias y Reemplazos.
5.7.3 Relaciones de Reescritura entre términos de la especificación.
5.7.4 Propiedad de Church-Roser: Confluencia y Terminancia.
5.8 Semántica por Clases de Equivalencia.
5.9 Resumen del capítulo.
5.10 Ejercicios propuestos.
Capítulo 6
6.1 Introducción.
6.2 Resolución.
6.2.1 Resolución en lógica proposicional.
6.2.1.1 Notación
6.2.1.2 Resolventes
6.2.1.3 Demostración por introducción de resolventes.
6.2.1.4 El teorema de Resolución
6.2.2 Resolución en Lógica de Predicados.
6.2.2.1 Notación
6.2.2.2 Unificación
6.2.2.3 Resolventes
6.3 El Lenguaje PROLOG visto desde la Lógica.
6.3.1 Cláusulas de Horn y programa PROLOG.
6.3.2 Consultas en PROLOG
6.3.3 Forma Prenex de un programa PROLOG
6.4 Sintaxis y nomenclatura del PROLOG
6.4.1 Términos.
6.4.1.1 Átomos
6.4.1.2 Literales
6.4.1.3 Variables
6.4.1.4 Términos Complejos
6.4.2 Predicados.
6.4.3 Programa: Hechos y Reglas.
6.4.3.1 Hechos
6.4.3.2 Reglas
6.4.4 Consultas
6.4.5 Ejemplo de PROLOG
6.5 Procesamiento por Resolución SLD.
6.5.1 Búsqueda de la prueba y árboles de búsqueda
6.5.2 Búsqueda de la prueba y tabla de reescritura de la consulta
6.6 Resumen del Capítulo.
6.7 Ejercicios propuestos
Capítulo 7
7.1 Introducción
7.2 Multiplicidad de Lenguajes
7.3 Conceptos diferenciadores de los lenguajes de programación.
7.4 Implementaciones e interfaces.
7.4.1 Linea de comandos REPL.
7.4.2 Ciclo Codificación Interpretación Ejecución.
7.5 Operadores nativos y Expresiones simples.
7.6 Resumen del Capítulo.
7.7 Ejercicios Propuestos.
Capítulo 8
8.1 Introducción
8.2 Justificación.
8.2.1 Reuso de código.
8.2.2 Arquitectura de funciones y de objetos.
8.3 Definición de los operadores.
8.3.1 Definición de Operadores en lenguajes Funcionales.
8.3.2 Definición de Operadores en lenguajes CLAUSALES.
8.3.3 Definición de Operadores en lenguajes PROCEDURALES.
8.4 Selección.
8.4.1 Selección por emparejamiento de la evocación formal con la evocación real.
8.4.2 Selección por condición de guardia sobre las unidades de especificación.
8.4.3 Operadores e instrucciones de selección.
8.5 Tipo del operador y de sus operandos
8.5.1 Perfil de los Operadores en SCHEME.
8.5.1.1 Predicado de Tipo
8.5.2 Perfil de los operadores en MAUDE
8.5.2.1 Declaraciones de sort y relaciones de subsort en MAUDE
8.5.2.2 Declaración de variables en MAUDE.
8.5.2.3 Declaración de operadores en MAUDE
8.5.2.3.1 Notación Prefija y Notación Infija
8.5.2.3.2 Constantes
8.5.2.3.3 Sobrecarga de Operadores.
8.5.2.3.4 Atributos Ecuacionales
8.5.2.3.5 Precedencia y gathering
8.5.3 Perfil de los Predicados en SWI PROLOG.
8.6 Medio ambiente y asignación.
8.6.1 Medio ambiente en SCHEME.
8.6.1.1 Introducción de Símbolos y de su Significado.
8.6.1.2 Cambio del Significado de un Símbolo.
8.6.1.3 Medio ambiente de una evocación.
8.6.1.4 Extensiones locales del medio ambiente durante el cálculo.
8.6.1.5 Faceta Procedural del SCHEME
8.6.2 Medio ambiente en MAUDE.
8.6.3 Medio ambiente en PROLOG.
8.7 Estrategia de Evaluación.
8.7.1 Estrategia de Evaluación en SCHEME.
8.7.2 Estrategia de evaluación en MAUDE
8.7.3 Estrategia de evaluación en PROLOG
8.8 Estructura de los programas.
8.8.1 Estructura de los programas en SCHEME
8.8.2 Estructura de los programas en MAUDE
8.8.2.1 Definición y contenido de módulos en MAUDE
8.8.2.2 Relaciones entre módulos en MAUDE
8.8.2.3 Inclusión de Módulos en MAUDE
8.8.2.4 Algebra de Módulos en MAUDE
8.9 Resumen del Capítulo.
8.10 Ejercicios Propuestos.
Capítulo 9
9.1 Introducción.
9.2 Ejemplos de Definición Recursiva de Operadores.
9.2.1 Sumatoria.
9.2.2 Raíz cuadrada por el método de Newton_Rapson.
9.3 La forma del Proceso de Cálculo (uso de memoria).
9.3.1 Forma del proceso: acumulador asociativo y no asociativo.
9.3.1.1 Acumulador recursivo
9.3.1.2 Acumulador iterativo
9.4 La precisión del proceso de Cálculo
9.4.1.1 Primer cambio al cálculo del coseno: mejora en la precisión.
9.5 La eficiencia del proceso de Cálculo.
9.5.1.1 Segundo cambio al cálculo del coseno: mejora en la eficiencia.
9.5.1.2 Tercer cambio al cálculo del coseno: precisión en la condición de salida
9.6 Serie de Fibonacci.
9.6.1 Proceso recursivo.
9.6.2 Proceso iterativo.
9.7 Utilidad de la recursión
9.8 Resumen del Capítulo.
9.9 Ejercicios propuestos.
Capítulo 10
10.1 Introducción
10.2 Tipos Compuestos Estructurados
10.2.1 Declaración de tipos compuestos estructurados.
10.2.1.1 Declaración de un tipo compuesto estructurado en SCHEME.
10.2.1.2 Declaración de un tipo compuesto estructurado en MAUDE
10.2.2 Construcción de instancias del tipo compuesto estructurado.
10.2.2.1 Construcción de instancias del tipo compuesto estructurado en SCHEME.
10.2.2.2 Construcción de instancias del compuesto estructurado en MAUDE
10.2.3 Selección de componentes de un valor compuesto estructurado.
10.2.3.1 Selección de componentes en SCHEME.
10.2.3.2 Selección de componentes en MAUDE
10.2.4 Definición de operadores sobre tipos compuestos estructurados.
10.2.4.1 Definición de operadores sobre tipos compuestos estructurados en SCHEME.
10.2.4.2 Definición de operadores sobre tipos compuestos estructurados en MAUDE.
10.2.4.2.1 Completitud suficiente en MAUDE
10.2.5 Invariantes de Tipo
10.2.5.1 Invariantes de tipo en SCHEME
10.2.5.2 Invariantes de Tipo en MAUDE.
10.3 Tipos Compuestos Iterados
10.3.1 Conexión entre componentes: Pares.
10.3.1.1 Parejas en SCHEME.
10.3.1.2 Parejas en MAUDE.
10.3.2 Estructura del iterado: conjuntos, listas, árboles y grafos.
10.4 Gestión de Listas.
10.4.1 Declaración de Listas.
10.4.1.1 Tipo nativo Lista en SCHEME.
10.4.1.2 Declaración de un tipo Lista en MAUDE
10.4.2 Constructores de la lista.
10.4.2.1 Constructores de listas en SCHEME.
10.4.2.2 Constructores de listas en MAUDE
10.4.2.3 Constructores de listas en PROLOG
10.4.3 Recorridos básicos sobre listas.
10.4.3.1 Recorridos básicos sobre Listas en SCHEME.
10.4.3.2 Recorridos básicos sobre Listas en MAUDE.
10.4.3.3 Recorridos básicos sobre Listas en PROLOG.
10.4.4 Selección sobre listas.
10.4.4.1 Selección sobre Listas en SCHEME.
10.4.4.2 Selección sobre Listas en MAUDE.
10.4.4.3 Selección sobre Listas en PROLOG.
10.4.5 Modificadores de la lista
10.4.5.1 Modificadores de listas en SCHEME.
10.4.5.2 Modificadores de listas en MAUDE.
10.4.5.3 Modificadores de listas en PROLOG.
10.4.6 Transformación de la lista
10.4.6.1 Transformación de listas en SCHEME.
10.4.6.2 Transformación de listas en MAUDE.
10.4.6.3 Transformación de listas en PROLOG.
10.5 Gestión de Árboles.
10.5.1 Ejemplo: Árbol Binario de Búsqueda.
10.5.2 Construcción del Árbol Binario de Búsqueda.
10.5.2.1 Construcción del Árbol en SCHEME.
10.5.2.2 Construcción del Árbol en MAUDE.
10.5.3 Localización de un Componente en el Árbol Binario de Búsqueda.
10.5.3.1 Localización de un Componente del Árbol en SCHEME.
10.5.3.2 Localización de un Componente del Árbol en MAUDE.
10.5.4 Inserción de un Componente en el Árbol Binario de Búsqueda.
10.5.4.1 Inserción de un Componente en el Árbol en SCHEME.
10.5.4.2 Inserción de un Componente en el Árbol en MAUDE.
10.6 Resumen del Capítulo.
10.7 Ejercicios propuestos
Capítulo 11
11.1 Introducción
11.2 Abstracción de tipo y operador en SCHEME.
11.2.1 Abstracción de tipo en SCHEME.
11.2.2 Abstracción de operadores en SCHEME.
11.2.2.1 Operadores como argumentos de otros operadores.
11.2.2.2 Expresiones lambda
11.2.2.3 Operadores como resultado de la evocación de operadores.
11.3 Abstracción de teorías en MAUDE.
11.3.1 Parametrización de módulos.
11.3.2 Definición de teorías.
11.3.3 Creación de vistas.
11.3.4 Creación de instancias de módulos paramétricos.
11.4 Relaciones entre Tipos.
11.4.1 “Kinds” y Gestión de Errores.
11.4.2 Sobrecarga de operadores en subtipos.
11.4.3 Preregularidad
11.4.4 Ecuaciones de Membresía y de Membresía Condicional
11.4.4.1.1 Lista Ordenable Paramétrica
11.4.5 Operadores Polimórficos y listas heterogéneas.
11.5 Resumen del Capítulo.
11.6 Ejercicios propuestos
Capítulo 12
12.1 Introducción.
12.2 Consultas Deductivas sobre una Base de Datos.
12.3 Búsqueda de datos y combinaciones de datos.
12.4 Acertijos
12.5 Resumen del Capítulo.