PDF de programación - Capítulo 1 Razonamiento automático

Capítulo 1

Razonamiento automático

J. A. Alonso Jiménez
A. Fernández Margarit
M. J. Pérez Jiménez

1.1 Introducción

En el presente trabajo hacemos un resumen histórico del razonamiento
automático y presentamos mediante un sistema de razonamiento auto-
mático distintas reglas, estrategias y aplicaciones.

1.2 Breve historia del razonamiento automático

Hacia finales del siglo XVII, Leibniz formula dos cuestiones que sinteti-
zan viejas aspiraciones del hombre:

• la necesidad de disponer de un lenguaje universal (lingua charac-

teristica) en el que poder expresar cualquier idea; y

• la posibilidad de mecanizar cualquier tipo de razonamiento (cal-

culus ratiocinator).

1

2

Capítulo 1. Razonamiento automático

Con el nacimiento de la Lógica Matemática moderna, en 1847, con los
trabajos de G. Boole y A. De Morgan, aparece un primer “rational cal-
culus”, en el sentido de Leibniz. Posteriormente, en 1869, S. Jevons
construye una máquina para verificar identidades booleanas.

La publicación en 1879 de los Begriffsschrift por parte de G. Frege,
marca el inicio de la formalización de la Lógica. Dicho texto se considera
precursor no sólo de los sistemas actuales de Lógica Matemática sino
también de todos los lenguajes formales. Paradójicamente, a pesar de
su importancia, estos trabajos pasaron desapercibidos.

Independientemente, G. Peano publica en 1889 sus Arithmetices Prin-
cipia en el que utiliza una nueva notación simbólica para formalizar la
teoría de números que R. Dedekind presentó el año anterior. La Ar-
itmética de Peano (PA) es una teoría de primer orden que recoge las
propiedades de los números naturales.

A principios del presente siglo, D. Hilbert propone usar las ideas de
Frege y Peano para fundamentar las Matemáticas. En 1910, B. Russell y
A. Whitehead publican el primer volumen de sus Principia Mathematica
en la línea propuesta por Hilbert.

La primera cuestión formulada por Leibniz, la necesidad de construir
un lenguaje universal, empezaba a tener respuestas parcialmente sa-
tisfactorias con los lenguajes formales. Hacia finales de los cincuenta,
con la irrupción de los computadores electrónicos y con el soporte de
los muchos logros obtenidos en el campo de la Lógica Matemática, se
retoma con fuerza el segundo objetivo de Leibniz: la automatización del
razonamiento, que se convierte en uno de los problemas iniciales de la
Inteligencia Artificial.

En 1957, A. Newell, J.C. Shaw y H.A. Simon presentan su “máquina
lógica” que consiste en un programa de computador capaz de probar 38
teoremas de la Lógica proposicional de los Principia Mathematica (tres
años antes, M. Davis había escrito un programa para demostrar teoremas
de la Aritmética de Presburger que no fue publicado en su momento).
En 1960, Hao Wang con sus programas consiguió demostrar 9 capítulos
de los Principia Mathematica en 9 minutos, incluyendo teoremas del
cálculo de predicados usando el sistema deductivo de Gentzen.

En el mismo año, Gilmore presenta otra forma de tratar el problema
de la deducción en la Lógica de primer orden basándose en un resul-
tado de Skolem y Herbrand que reduce la demostración de una fórmula
de primer orden, F , a la de una fórmula proposicional, F , asociada a
ella. En esta reducción aparecen dos problemas: (1) La búsqueda de un
“candidato” proposicional, F , y (2) la demostración de F .

1.3. Ejemplos de razonamiento automático con OTTER

3

El artículo “A computing procedure for quantification theory”, publi-
cado por M. Davis y H. Putnam en 1960, supuso un avance cualitativo
en la solución del problema (2) al introducir el concepto de cláusula y
reducir la demostración de primer orden al estudio de la consistencia
de conjuntos finitos de cláusulas proposicionales, proporcionando reglas
que simplifican dicho estudio.

Los intentos de obtener una solución satisfactoria al problema (1)
hacen emerger el concepto de unificación, que subyace en los trabajos
de Prawitz, y culmina en el trabajo “A machine oriented logic based
on the resolution principle” de J.A. Robinson publicado en 1965. En el
mismo, presenta el principio de resolución en el que se combina la regla
de corte proposicional y la unificación. Este trabajo supuso un hito
en la demostración automática de teoremas y, en cierto modo, puede
considerarse como el inicio de la deducción automática.

Desde entonces se han introducido diversos refinamientos del prin-
cipio de resolución encaminados a mejorar la potencia del mismo en
ciertos casos, y se han proporcionado estrategias para orientar el proceso
y acotar el espacio de búsqueda. Entre los refinamientos y estrategias,
destacamos los siguientes:

– Estrategia del conjunto soporte (L. Wos, D. Carson y G. Ro-

binson, 1965).

– Hiper–resolución (J.A. Robinson, 1965).

– Demodulación (L. Wos, G. Robinson, D. Carson y L. Shalla,

1967).

– Paramodulación (G. Robinson y L. Wos, 1969).

– Resolución UR y estrategia de pesos (J. McCharen, R. Over-

beek y L. Wos, 1976).

que comentaremos en la siguiente sección.

1.3 Ejemplos de razonamiento automático con

OTTER

OTTER (Organized Techniques for Theorem–proving and Effective
Research) es un demostrador automático de teoremas para la lógica de
primer orden con igualdad, desarrollado por W. McCune en 1988. En

4

Capítulo 1. Razonamiento automático

esta sección mostraremos cómo puede usarse OTTER para resolver dis-
tintos problemas que nos servirán para presentar las reglas y estrategias
que hemos comentado anteriormente.

1.3.1 Inconsistencia de cláusulas proposicionales y reso-

lución binaria

El primer problema que vamos a considerar consiste en determinar si
un conjunto dado de fórmulas proposicionales es inconsistente (es decir,
carece de modelos).
Ejemplo 1 Determinar si el conjunto

{P ∨ Q,¬P ∨ Q, P ∨ ¬Q,¬P ∨ ¬Q}

es inconsistente.

Para resolver el problema con OTTER tenemos que precisar dos
cuestiones: la primera es sintáctica (cómo se representa el problema en
OTTER) y la segunda es deductiva (qué regla de inferencia se usa para
resolverlo).

En OTTER se usa el lenguaje de cláusulas. Una cláusula es una
disyunción de literales positivos (i.e. fórmulas atómicas) y literales
negativos (i.e. negaciones de fórmulas atómicas). La negación se rep-
resenta por - y la disyunción por |. Las cláusula terminan en un punto.
El conjunto de las clásusulas se escriben entre las expresiones list(sos)
y end_of_list.

La regla de inferencia que usaremos es la resolución binaria pro-
posicional: a partir de dos cláusulas que contengan literales comple-
mentarios (i.e. que uno sea la negación del otro) obtener una nueva
cláusula haciendo la disyunción de sus literales excepto los complemen-
tarios; es decir,

L1 |...| Li |
A | L{i+1} |...| Ln
M1 |...| Mj | - A | M{j+1} |...| Mk
-------------------------------------------------------------
L1 |...| Li | L{i+1} |...| Ln | M1 |...| Mj | M{j+1} |...| Mk

donde las dos primeras reglas son las premisas (o cláusulas padres) y
la tercera es la conclusión (o resolvente). La regla de resolución bina-
ria es adecuada (es decir, la conclusión es consecuencia lógica de las
premisas). Por tanto, una forma de demostrar que el conjunto dado es

1.3. Ejemplos de razonamiento automático con OTTER

5

inconsistente es obtener nuevas cláusulas por resolución hasta llegar a
una contradicción.

En OTTER la expresión set(binary_res) indica que se usa la regla

de resolución binaria.

Una vez que sabemos cómo se representa en OTTER el problema
y cómo se indica la regla de inferencia que deseamos utilizar, vamos a
ver cómo se obtiene la solución. Para ello, se crea un archivo con la
representación del problema y la regla que se usa para resolverlo. En
este caso, creamos el archivo EJ1.IN, cuyo contenido es el siguiente:

list(sos).
P | Q.
-P | Q.
P | -Q.
-P | -Q.
end_of_list.
set(binary_res).

La demostración de la inconsistencia se obtiene mediante la siguiente
orden

otter <ej1.in >ej1.out

Con la cual se ejecuta OTTER tomando como archivo de entrada el
EJ1.IN y dirigiendo la salida al archivo EJ1.OUT, en el que se encuentra
la siguiente demostración:

.

1 [] P|Q.
2 [] -P|Q.
3 [] P| -Q.
4 [] -P| -Q.
5 [binary,2.1,1.1] Q.
6 [binary,3.2,5.1] P.
7 [binary,4.1,6.1] -Q.
8 [binary,7.1,5.1] $F.

Veamos cómo se interpreta la demostración. Las cuatro primeras cláu-
sulas son cláusulas de entrada (las del archivo EJ1.IN). La cláusula 5
se obtiene de la 1 y la 2 aplicando resolución binaria sobre sus primeros
literales. Análogamente se interpretan las líneas siguientes. En la 8 se
obtiene la cláusula vacía (representada por $F), con lo que se prueba
que el conjunto inicial es inconsistente.

6

Capítulo 1. Razonamiento automático

1.3.2 Inconsistencia de cláusulas de primer orden y uni-

ficación

Vamos a generalizar el problema anterior al caso de la lógica de primer
orden y comprobaremos cómo mediante sustituciones adecuadas (unifi-
cadores de máxima generalidad) se reduce al caso anterior. Para ello
consideramos el siguiente
Ejemplo 2 Demostrar que el conjunto

{¬P (x) ∨ Q(x), P (a),¬Q(z)}

es inconsistente.

Procediendo como en el Ejemplo 1, escribimos en el archivo de en-

trada

list(sos).
-P(x) | Q(x).
P(a).
-Q(z).
end_of_list.
set(binary_res).

y obtenemos la demostración

1 [] -P(x)|Q(x).
2 [] P(a).
3 [] -Q(z).
4 [binary,1.1,2.1] Q(a).
5 [binary,4.1,3.1] $F.

Nótese que para obtener la cláusula 4 se aplica a la 1 la sustitución
{x/a} que es un unificador de máxima generalidad de los literales
P(x) y P(a) (es decir, la sustitución más que general que aplicada a
ambos literales los hace idénticos). La forma de la resolución binaria
de primer orden es

L1 |...| Li |
A | L{i+1} |...| Ln
M1 |...| Mj | - B | M{j+1} |...| Mk
----------------------------------------------------------------
(L1 |...| Li | L{i+1} |...| Ln | M1 |...| Mj | M{j+1} |...| Mk)s

donde s es un unificador de