Lógica para la Computación

Argumento de Lógica para la Computación

La fuerza de la Lógica Formal reside en su capacidad para. deducir precisa y, en muchos casos, mecánicamente, ciertas expresiones simbólicas nuevas a partir de otras anteriores. Las expresiones inferidas son los teoremas

Así se abre el texto: con los símbolos y leyes lógicas que nos enseñarán a usar el sentido común y nuestra capacidad de razonar sobre la realidad. Con ellos, demostraremos teoremas con rigor y, mejor aún, aprenderemos a verificar con precisión que son realmente válidos.

Estamos así en pleno centro de las Teorías de primer orden, la base de toda lógica; aparecen sus raíces sanas y fuertes desde hace más de un siglo y se muestran resultados históricos tanto por su propia importancia como por su papel en el desarrollo de la ciencia moderna.

Con tales mimbres y a partir de su propio trabajo científico y experiencia docente en Lógica, el autor ha hecho de estas primeras nociones una base para el desarrollo posterior del texto.

El lector que se sitúa en este punto inicial comienza el tránsito a lo largo de una línea de la que no se separará y que le conduce con claridad hasta los fundamentos y las primeras nociones de la programación lógica y PROLOG. Para el camino se le proporciona todo el equipaje necesario, pero nada más. Tendrá que asomarse a nuevos sistemas formales con su correspondiente teoría y nada será superfluo porque pronto verá cómo dicha teoría tiene la potencia necesaria para ir haciendo la Lógica cada vez más algorítmica.

Este libro no es sobre la historia. Tales libros, salvo ejercicios de estilo, tienen la servidumbre de presentarse como un todo acabado. Sin embargo, el autor no ha olvidado que a todos nos gusta saber cómo han surgido las cosas y por qué alguien demostró lo que demostró.

Por eso, ha procurado que el lector nunca olvide que está en un camino, ha añadido los comentarios que ha creído oportunos y ha escrito con la intención de facilitar la lectura en la medida de lo posible.

Este es un texto pensado para estudiantes y profesores inclinados a las matemáticas, la lógica y los fundamentos de su automatización, alumnos de primeros cursos de Lógica y aquellos programadores de PROLOG que no han tenido la oportunidad de asomarse a la base sobre la que descansa su trabajo.

El libro tiene un aire a la vez nuevo y tradicional que lo hace muy recomendable para aquellos a los que está destinado Eugenio Roanes Lozano, Reseña en el Boletín de la Sociedad \"Puig Adam\" de Profesores de Matemáticas.0INTRODUCCIÓN

CAPÍTULO 1. TEORÍAS DE PRIMER ORDEN
1.1 TEORÍAS DE PRIMER ORDEN
1.1.1 Lenguajes de primer orden
1.1.2 El sistema formal teorías de primer orden
1.1.3 Meta teoremas. Reglas y teoremas derivados
1.2 EL CÁLCULO DE TABLAS ANALÍTICAS
1.2.1 Definiciones y utilización
1.2.2 Aplicación
1.3 SEMÁNTICA
1.3.1 Estructuras
1.3.2 Significado de expresiones
1.3.3 Validez
1.4 COMPLETUD, CONSISTENCIA Y DECIDIBILIDAD
1.5 LA LÓGICA DE PROPOSICIONES
1.5.1 Sintaxis
1.5.2 Semántica
1.5.3 Cláusulas de Horn

CAPÍTULO 2. RESOLUCIÓN
2.1 REDUCCIÓN A UN CONJUNTO DE CLÁUSULAS
2.1.1 Formas Prenex
2.1.2 Formas de Skolem
2.1.3 Supresión de cuantificadores universales
8 LÓGICA PARA LA COMPUTACIÓN © RA-MA
2.1.4 Reducción a un conjunto de cláusulas
2.2 UNIFICACIÓN
2.3 RESOLUCIÓN Y TEORÍA DE HERBRAND
2.3.1 Principio de resolución
2.3.2 Corrección
2.3.3 Teoría de Herbrand
2.3.4 Completud
2.4 ALGUNOS PROCEDIMIENTOS BASADOS EN EL TEOREMA DE HERBRAND

CAPÍTULO 3. ELEMENTOS DE PROGRAMACIÓN LÓGICA Y PROLOG
3.1 REFINAMIENTO Y ESTRATEGIAS DE LA RESOLUCIÓN
3.1.1 La resolución SLD
3.1.2 Utilización de la resolución SLD y otros refinamientos
3.2 PROLOG
3.2.1 La resolución PROLOG
3.2.2 Búsqueda en profundidad
3.2.3 Búsqueda en anchura
3.2.4 Las ramas infinitas
3.2.5 La vuelta atrás
3.2.6 Predicados y funciones de la implementación

APÉNDICE A. DEFINICIONES Y DEMOSTRACIONES INDUCTIVAS
A.1 DEFINICIONES INDUCTIVAS
A.2 DEMOSTRACIONES INDUCTIVAS
APÉNDICE B. ADECUACIÓN DE LAS TABLAS ANALÍTICAS
APÉNDICE C. CONSIDERACIONES ELEMENTALES SOBRE LA REPRESENTACIÓN DEL CONOCIMIENTO CON LENGUAJES DE PRIMER ORDEN
C.1 PREPARACIÓN
C.2 REPRESENTACIÓN
REFERENCIAS
ÍNDICE ALFABÉTICO