PDF de programación - Introducción al razonamiento automático con OTTER

Introducción al razonamiento automático con

OTTER

José A. Alonso Jiménez

Grupo de Lógica Computacional
Dpto. de Ciencias de la Computación e Inteligencia Artificial
Universidad de Sevilla
Sevilla, 1 de septiembre de 2006 (versión de 5 de noviembre de 2006)

2

José A. Alonso Jiménez

Esta obra está bajo una licencia Reconocimiento–NoComercial–CompartirIgual 2.5 Spain de Crea-
tive Commons.

Se permite:

copiar, distribuir y comunicar públicamente la obra

hacer obras derivadas

Bajo las condiciones siguientes:

Reconocimiento. Debe reconocer los créditos de la obra de la manera especificada
por el autor.

No comercial. No puede utilizar esta obra para fines comerciales.

Compartir bajo la misma licencia. Si altera o transforma esta obra, o genera una
obra derivada, sólo puede distribuir la obra generada bajo una licencia idéntica a
ésta.

Al reutilizar o distribuir la obra, tiene que dejar bien claro los términos de la licencia de
esta obra.

Alguna de estas condiciones puede no aplicarse si se obtiene el permiso del titular de los
derechos de autor.

Esto es un resumen del texto legal (la licencia completa). Para ver una copia de esta licencia,
visite http://creativecommons.org/licenses/by-nc-sa/2.5/es/ o envie una carta a Creative
Commons, 559 Nathan Abbott Way, Stanford, California 94305, USA.

Introducción al razonamiento automático con OTTER

Resumen

OTTER (Organized Techniques for Theorem–proving and Effective Research) es un de-
mostrador automático de teoremas para la lógica de primer orden con igualdad, desarrollado
por W. McCune en 1988. En esta trabajo mostraremos cómo puede usarse OTTER para resolver
distintos problemas que nos servirán para presentar las reglas y estrategias de razonamiento.

Índice

1. Inconsistencia de cláusulas proposicionales y resolución binaria

2. Inconsistencia de cláusulas de primer orden y unificación

3. Inconsistencia de fórmulas de primer orden y skolemización

4. Consecuencia lógica

5. Validez de argumentaciones y representación del conocimiento

6. La estrategia del conjunto soporte

7. Resolución UR

8. Hiper–resolución

9. Obtención de respuestas

10. Validez de argumentaciones con igualdad

11. Paramodulación

12. Demodulación

13. Modo autónomo

14. Conclusiones

15. Bibliografía.

3

3

4

5

6

6

7

8

9

10

11

14

14

17

18

19

4

1.

José A. Alonso Jiménez

Inconsistencia de cláusulas proposicionales y resolución bi-
naria

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 po-
sitivos (i.e. fórmulas atómicas) y literales negativos (i.e. negaciones de fórmulas atómicas). La
negación se representa por - y la disyunción por |. Las cláusulas terminan en un punto. El con-
junto 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 proposicional: a partir de dos
cláusulas que contengan literales complementarios (i.e. que uno sea la negación del otro) obtener
una nueva cláusula haciendo la disyunción de sus literales excepto los complementarios; 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 binaria 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 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

Introducción al razonamiento automático con OTTER

5

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áusulas son cláusulas de en-
trada (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 inconsis-
tente.

2.

Inconsistencia de cláusulas de primer orden y unificación

Vamos a generalizar el problema anterior al caso de la lógica de primer orden y comprobare-
mos cómo mediante sustituciones adecuadas (unificadores 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 entrada

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

6

José A. Alonso Jiménez

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 máxima generalidad de los literales A y B.

3.

Inconsistencia de fórmulas de primer orden y skolemización

Vamos a extender el problema al caso en que el conjunto de fórmulas no estén en forma de
cláusulas. Mediante el procedimiento de Skolem, dado un conjunto de fórmulas S se construye
un conjunto de cláusulas S0 tal que S es inconsistente precisamente si S0 es inconsistente (es decir,
S y S0 son equiconsistentes). Lo ilustraremos con el siguiente
Ejemplo 3 Demostrar que el conjunto de fórmulas {(∀x)[P(x) → Q(x)], P(a),¬(∃z)Q(z)} es incon-
sistente.

En OTTER también se puede usar el lenguaje lógico primer orden. En este caso, los símbolos
lógicos que se necesitan son el condicional (que se representa por ->), el cuantificador universal
(que se representa por all) y el cuantificador existencial (que se representa exists). Además,
para indicar que se usan fórmulas en lugar de cláusulas, se escribe formula_list(sos) en lugar
de list(sos).

El archivo de entrada correspondiente al Ejemplo 3 es

formula_list(sos).

all x (P(x) -> Q(x)).
P(a).
-(exists z Q(z)).

end_of_list.

set(binary_res).

Al ejecutar OTTER con dicho archivo, lo primero que hace es transformar el conjunto de fór-
mulas en un conjunto de cláusulas equiconsistente (utilizando funciones y constantes de Skolem
para eliminar cuantificadores existenciales). Una vez realizada la transformación el problema se
reduce al anterior. La demostración obtenida es

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.

Introducción al razonamiento automático con OTTER

7

4. Consecuencia lógica

Hasta ahora hemos visto problemas de inconsistencia. El problema de consecuencia lógica
(es decir, dado un conjunto de fórmulas S determinar si la fórmula F es consecuencia lógica de S)
se reduce al de inconsistencia, ya que F es consecuencia lógica de S precisamente si S ∪ {¬F} es
inconsistente.

5. Validez de argumentaciones y representación del conocimien-

to

La decisión de la validez de una argumentación presenta dos nuevos problemas: uno es el
problema de la representación del conocimiento y el otro es la explicitación del conocimiento
implícito. Vamos a verlo en el siguiente

Ejemplo 4 Demostrar la validez del siguiente argumento: Los caballos son más rápidos que los perros.
Algunos galgos son más rápidos que los conejos. Lucero es un caballo y Orejón es un conejo. Por tanto,
Lucero es más rápido que Orejón.

Comenzamos determinando los símbolos de constantes que usaremos para la representación

del argumento. Son los siguientes:
Lucero
Orejón
x es un caballo
x es un conejo
x es un galgo
x es un perro

Lucero
Orejon
CABALLO(x)
CONEJO(x)
GALGO(x)
PERRO(x)
MAS_RAPIDO(x,y) x es más rápido que y

Por lo que respecta al lenguaje, utilizamos por primera vez la conjunción (&). Con este lenguaje
las cuatro primeras fórmulas representan las hipótesis del argumento; la quinta, la negación de la
conclusión y las dos últimas, información implícita necesaria para la demostración. El archivo de
entrada es

formula_list(sos).

all x y (CABALLO(x) & PERRO(y) -> MAS_RAPIDO(x,y)).
exists x (GALGO(x) & (all y (CONEJO(y) -> MAS_RAPIDO(x,y)))).
CABALLO(Lucero).
CONEJO(Orejon).
-MAS_RAPIDO(Lucero,Orejon).
all x (GALGO(x) -> PERRO(x)).
all x y z (MAS_RAPIDO(x,y) & MAS_RAPIDO(y,z) -> MAS_RAPIDO(x,z)).

end