PDF de programación - Deducción automática (Vol. 1: Construcción lógica de sistemas lógicos)

Deducción automática

(Vol. 1: Construcción lógica de sistemas lógicos)

José A. Alonso Jiménez y Joaquín Borrego Díaz

Dpto. de Ciencias de la Computación e Inteligencia Artificial

Universidad de Sevilla

30 de diciembre de 2002

2

Índice General

Prólogo

1 Prólogo

2 Introducción a la programación lógica con Prolog

2.2 Listas

2.1 El sistema deductivo de Prolog . . . . . . . . . . . . . . . . . .
. . . . . . . .
2.1.1 Deducción Prolog en lógica proposicional
2.1.2 Deducción Prolog en lógica relacional
. . . . . . . . . .
2.1.3 Deducción Prolog en lógica funcional . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2.1 Representación de listas . . . . . . . . . . . . . . . . . .
2.2.2 Concatenación de listas
. . . . . . . . . . . . . . . . . .
2.2.3 La relación de pertenencia . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3 Disyunciones
2.4 Operadores
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.5 Aritmética . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.6 Control mediante corte . . . . . . . . . . . . . . . . . . . . . . .
2.7 Negación . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.8 El condicional . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.9 Predicados sobre tipos de término . . . . . . . . . . . . . . . .
2.10 Comparación y ordenación de términos . . . . . . . . . . . . . .
2.11 Procesamiento de términos
. . . . . . . . . . . . . . . . . . . .
2.12 Procedimientos aplicativos . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . .
2.13 Todas las soluciones

3

6

7

9
9
9
14
15
19
20
21
23
24
24
26
27
31
34
35
36
38
40
41

4

Índice General

3 Elementos de lógica proposicional

3.1 Sintaxis de la lógica proposicional . . . . . . . . . . . . . . . . .
3.2 Valores de verdad . . . . . . . . . . . . . . . . . . . . . . . . . .
3.3 Funciones de verdad . . . . . . . . . . . . . . . . . . . . . . . .
3.4 Valor de una fórmula en una interpretación . . . . . . . . . . .
3.5
Interpretaciones principales de una fórmula . . . . . . . . . . .
3.6 Modelo de una fórmula . . . . . . . . . . . . . . . . . . . . . . .
3.7 Cálculo de los modelos de una fórmula . . . . . . . . . . . . . .
3.8 Satisfacibilidad . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.9 Satisfacibilidad con MACE . . . . . . . . . . . . . . . . . . . .
3.10 Contramodelo de una fórmula . . . . . . . . . . . . . . . . . . .
3.11 Validez. Tautologías . . . . . . . . . . . . . . . . . . . . . . . .
3.12 Satisfacibilidad y validez . . . . . . . . . . . . . . . . . . . . . .
3.13 Interpretaciones principales de un conjunto de fórmulas
. . . .
3.14 Modelo de un conjunto de fórmulas . . . . . . . . . . . . . . . .
3.15 Cálculo de modelos de conjuntos de fórmulas
. . . . . . . . . .
3.16 Consistencia de un conjunto de fórmulas . . . . . . . . . . . . .
3.17 Consistencia con MACE . . . . . . . . . . . . . . . . . . . . . .
3.18 Consecuencia lógica . . . . . . . . . . . . . . . . . . . . . . . .
3.19 Consecuencia lógica e inconsistencia . . . . . . . . . . . . . . .
3.20 Consecuencia lógica con MACE . . . . . . . . . . . . . . . . . .
3.21 Aplicaciones del razonamiento proposicional . . . . . . . . . . .

4 Sistemas deductivos proposicionales

4.1 Tableros semánticos

. . . . . . . . . . . . . . . . . . . . . . . .
4.1.1 Ejemplos de demostraciones por tableros semánticos . .
4.1.2 Notación uniforme . . . . . . . . . . . . . . . . . . . . .
4.1.3 Procedimiento de completación de tableros
. . . . . . .
4.1.4 Tableros cerrados . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . .
4.1.5 Teorema por tableros
4.1.6 Deducción por tableros
. . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2.1 Equivalencia lógica . . . . . . . . . . . . . . . . . . . . .
4.2.2 Forma normal negativa . . . . . . . . . . . . . . . . . .
4.2.3 Forma normal conjuntiva . . . . . . . . . . . . . . . . .
4.2.4 Transformación a cláusulas
. . . . . . . . . . . . . . . .
4.2.5 Transformación a cláusulas con OTTER . . . . . . . . .

4.2 Cláusulas

43
43
45
45
46
47
49
50
51
52
53
53
54
54
56
56
57
58
58
59
60
61

75
75
75
76
78
81
81
82
84
84
84
86
88
90

Índice General

4.3 Resolución . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3.1 Motivación de resolución . . . . . . . . . . . . . . . . . .
4.3.2 Regla de resolución proposicional . . . . . . . . . . . . .
4.3.3 Demostraciones por resolución . . . . . . . . . . . . . .
4.3.4 Procedimiento elemental de búsqueda de refutación . . .
4.3.5 Resolución con OTTER . . . . . . . . . . . . . . . . . .
4.3.6 Resolución de OTTER en Prolog . . . . . . . . . . . . .

Bibliografía

5

91
91
92
93
94
95
99

103

6

Índice General

Capítulo 1

Prólogo

Este libro constituye el primer volumen de una serie sobre deducción au-
tomática. Su objetivo es la presentación de Prolog como un sistema de de-
ducción automática y la construcción en Prolog de sistemas de deducción pro-
posicional.

En el primer capítulo presentamos la programación lógica en Prolog co-
mo una aplicación de la deducción automática a la vez que se introducen los
conocimientos de Prolog necesarios en los siguientes capítulos del libro.

En el segundo capítulo se formaliza en Prolog los conceptos básicos de la
lógica proposicional y se muestra cómo pueden resolverse algunos problemas
con OTTER y MACE.

En el tercer capítulo se construyen en Prolog distintos cálculos lógicos pro-

posicionales.

En los siguientes volúmenes continuaremos la construcción de sistemas lógi-
cos (para la lógica de primer orden con igualdad), estudiaremos el razonamiento
asistido por ordenador (con OTTER, MACE y ACL2) y aplicaciones del razo-
namiento automático.

El material de este volumen y los siguientes forma parte de cursos impar-
tidos por los autores en el Departamento de Ciencias de la Computación e
Inteligencia Artificial de la Universidad de Sevilla. Se puede acceder a dichos
cursos en la Red a través de http://www.cs.us.es/~jalonso.

7

8

Capítulo 1. Prólogo

Capítulo 2

Introducción a la
programación lógica con
Prolog

En este capítulo presentamos el lenguaje de programación lógica Prolog con
un doble objetivo: como una aplicación de la deducción automática y como
soporte para la construcción de los sistemas lógicos que realizaremos en los
siguientes capítulos.

Los textos fundamentales de Prolog son [2], [5], [10] y [11].

2.1 El sistema deductivo de Prolog

En esta sección vamos a presentar el procedimiento básico de deducción de Pro-
log: la resolución SLD. La presentación la haremos ampliando sucesivamente
la potencia expresiva del lenguaje considerado.

2.1.1 Deducción Prolog en lógica proposicional

En esta sección vamos a estudiar el sistema deductivo de Prolog en el caso de
la lógica proposicional. Vamos a desarrollar el estudio mediante el siguiente
ejemplo.

9

10

Capítulo 2.

Introducción a la programación lógica con Prolog

Ejemplo 2.1.1 [Problema de clasificación de animales]
Disponemos de una base de conocimiento compuesta de reglas sobre clasifica-
ción de animales y hechos sobre características de un animal.

• Regla 1: Si un animal es ungulado y tiene rayas negras, entonces es una

cebra.

• Regla 2: Si un animal rumia y es mamífero, entonces es ungulado.
• Regla 3: Si un animal es mamífero y tiene pezuñas, entonces es ungulado.
• Hecho 1: El animal tiene es mamífero.
• Hecho 2: El animal tiene pezuñas.
• Hecho 3: El animal tiene rayas negras.

Demostrar a partir de la base de conocimientos que el animal es una cebra.

Demostración: Una forma de demostrarlo es razonando hacia atrás. El pro-
blema inicial consiste en demostrar que el animal es una cebra. Por la regla
1, el problema se reduce a demostrar que el animal es ungulado y tiene rayas
negras. Por la regla 3, el problema se reduce a demostrar que el animal es
mamífero, tiene pezuñas y tiene rayas negras. Por el hecho 1, el problema se
reduce a demostrar que el animal tiene pezuñas y tiene rayas negras. Por el
hecho 2, el problema se reduce a demostrar que el animal tiene rayas negras.

Que es cierto por el hecho 3.
Para resolver el problema anterior con Prolog tenemos que considerar las si-
guientes cuestiones: (1) cómo se representan las reglas, (2) cómo se representan
los hechos, (3) cómo se representan las bases de conocimientos en Prolog, (4)
cómo se inicia una sesión Prolog, (5) cómo se carga la base de conocimiento, (6)
cómo se plantea el objetivo a demostrar y (7) cómo se interpreta la respuesta.
Una vez resuelto, se plantean las siguientes cuestiones: (8) cómo ha realizado
Prolog la búsqueda de la demostración, (9) cuál la demostración obtenida y
(10) como se corresponde dicha demostración con la anteriormente presentada.
Para representar una regla, se empieza por elegir los símbolos para los
átomos que aparecen en la regla. Para la regla 1, podemos elegir los símbolos
es_ungulado, tiene_rayas_negras y es_cebra. La regla 1 puede represen-
tarse como

Si es_ungulado y tiene_rayas_negras entonces es_cebra

2.1. El sistema deductivo de Prolog

11

Usando las conectivas lógicas la expresión anterior se escribe mediante la fórmula

es_ungulado ∧ tiene_rayas_negras → es_cebra

donde ∧ representa la conjunción y →, el condicional. La fórmula anterior se
representa en Prolog, mediante la cláusula

es_cebra :- es_ungulado, tiene_rayas_negras.

Se puede observar que la transformación ha consistido en invertir el sentido
de la escritura y sustituir las conectivas por :- (condicional inversa) y , (con-
junción). El átomo a la izquierda de :- se llama la cabeza y los átomos a la
derecha se llama el cuerpo de la regla.

Para representar los hechos basta elegir los símbolos de