Introducció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 decidibilldad

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
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 Cornpletud

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