Ejercicio 4: Prueba de teoremas en lógica de predicados.
OTTER
El ejercicio consiste en resolver un par de demostraciones en Lógica de Primer Orden utilizando un probador de teoremas (OTTER)
por refutación mediante la técnica de resolución. Aunque
OTTER permite la introducción de fórmulas arbitrarias, en
realidad las convierte primero a Forma Normal de Skolem y luego a CNF.
En nuestro caso, sin embargo, haremos a mano esta conversión y
facilitaremos directamente a OTTER la lista de cláusulas CNF.
La sintaxis es bastante sencilla:
- la negación se representa con el símbolo menos '-'
- la disyunción se representa con la barra vertical '|'
- las variables son cualquier identificador que comience por u, v, w, x, y, z.
- cada cláusula debe finalizar con un punto.
- las líneas de comentarios comienzan con un '%'
Por último, las cláusulas van delimitadas por un par de sentencias del estilo:
list(...).
... cláusulas ...
end_of_list.
El tipo de "list" puede ser, entre otros valores, "usable" o "sos" (set
of support, es decir, cláusulas a usar preferentemente). Si no
queremos tomar ninguna decisión de preferencia para la
búsqueda, añadiremos al principio la línea:
set(auto).
Como prueba, veamos como se representaría el ejemplo
clásico: todo hombre es mortal; Sócrates es un hombre;
luego Sócrates es mortal. El contenido del fichero de entrada, socrates.in, sería el siguiente
set(auto).
list(usable).
-Hombre(x) | Mortal(x). % Todo hombre es mortal
Hombre(Socrates). % Sócrates es un hombre
-Mortal(Socrates). % Luego Sócrates es mortal
%(lo negamos para refutación)
end_of_list.
Para ejecutarlo, usamos el fichero ejecutable otter (para Solaris), del siguiente modo:
$ otter < socrates.in >socrates.out
o simplemente
$ otter < socrates.in
si queremos la salida por pantalla. En este ejemplo, la salida contiene las líneas:
---------------- PROOF ----------------
1 [] -Hombre(x)|Mortal(x).
2 [] -Mortal(Socrates).
3 [] Hombre(Socrates).
4 [hyper,3,1] Mortal(Socrates).
5 [binary,4.1,2.1] $F.
------------ end of proof -------------
donde lo relevante es la
obtención de $F, que es la forma de indicar la constante
"falso", o lo que es equivalente, la cláusula vacía en
CNF. Esto significa que el conjunto de fórmulas es inconsistente
y, dado que habíamos negado la conclusión original que
deseábamos comprobar (Mortal(Socrates)), quiere decir que ésta se sigue de las dos primeras premisas.
Como prueba, podemos establecer
algunas preferencias en el control de búsqueda de forma manual.
Por ejemplo, vamos a usar ahora resolución binaria y
añadir todas las fórmulas al conjunto
set of support.
set(binary_res).
list(sos).
-Hombre(x) | Mortal(x).
Hombre(Socrates).
-Mortal(Socrates).
end_of_list.
Si nos fijamos en la prueba obtenida:
---------------- PROOF ----------------
1 [] -Hombre(x)|Mortal(x).
2 [] Hombre(Socrates).
3 [] -Mortal(Socrates).
4 [binary,1.1,2.1] Mortal(Socrates).
5 [binary,4.1,3.1] $F.
------------ end of proof -------------
vemos que la cláusula 4 se obtiene de hacer resolución
entre 1.1 (cláusula 1, literal 1) y 2.1 (cláusula 2,
literal 1). El unificador aplicado no aparece indicado: en este caso es
sustituir la variable x por Socrates.
Típicamente, sin embargo, se suele usar como set of support inicial
solamente la cláusula que representa la conclusión
(negada) que queremos probar, en este caso, la cláusula 3. Esto
se hace para dirigir la prueba hacia el objetivo que se desea probar.
En nuestro ejemplo, tendríamos:
set(binary_res).
list(usable).
-Hombre(x) | Mortal(x).
Hombre(Socrates).
end_of_list.
list(sos).
-Mortal(Socrates).
end_of_list.
Si echamos un vistazo a la prueba
obtenida, veremos ahora que ésta comienza usando
-Mortal(Socrates) y procede a obtener -Hombre(Socrates), razonando
"hacia atrás".
---------------- PROOF ----------------
1 [] -Hombre(x)|Mortal(x).
2 [] Hombre(Socrates).
3 [] -Mortal(Socrates).
4 [binary,3.1,1.2] -Hombre(Socrates).
5 [binary,4.1,2.1] $F.
------------ end of proof -------------
Práctica Obligatoria 2:
Ej1) Se desea comprobar si, dadas las siguientes premisas:
- Algún estudiante de informática asiste a todos los congresos de lógica.
- Ningún estudiante de informática asiste a una reunión sin interés.
se puede demostrar que, por lo tanto:
- Ningún congreso de lógica es una reunión carente de interés.
Ej2) Comprobar ahora el siguiente ejemplo, extraído del libro [Russell&Norvig03]:
- Todo aquel que ama a todos los animales es amado por alguien.
- Aquel que mata a un animal no es amado por nadie.
- Jack ama a todos los animales.
- O bien Jack, o bien la Curiosidad mataron al gato, que se llama Tuna.
- ¿La Curiosidad mató al gato?
Plazo de entrega: 31 enero 2005.
[Russell&Norvig03] S. Russell and P. Norvig, Artificial Intelligence: a modern approach (2nd ed.), Prentice-Hall, 2003.