La práctica consiste en el uso del probador
de teoremas Otter para el diseño y construcción de
un sistema de representación del conocimiento y de razonamiento
basados en lógica de predicados. Otter es un sistema de deducción
automática desarrollado en la Mathematics and Computer Science Division
del Argonne National Laboratory.
Las reglas de inferencia de Otter están basadas en resolución y paramodulación e incluye muchas otras técnicas y estrategias para dirigir y restringir la búsqueda de pruebas. Las pruebas las realiza por refutación e implementa unificación para manejar variables. Otter usa la forma clausal para representar la información, de tal manera que todas las claúsulas forman una conjunción implicitamente.
Notas sobre representación de conocimiento en Otter.
La práctica a realizar supone una breve introducción
a Otter y su uso en Representación de Conocimiento y Razonamiento
sin preocuparnos de su uso en la prueba de teoremas matemáticos.
Los fuentes de Otter, manuales, versiones para sistemas Unix,
Mac y Windows, y bibliografía sobre sistemas de deducción
automática y sobre los resultados en investigación matemática
obtenidos por Otter pueden encontrarse en las paginas web de Otter. En primer lugar el estudiante debe bajar e instalar Otter. Mi instalación sobre Linux requirió menos de 13MB de espacio de disco (menos de 10MB borrando el "gzipped tar archive" antes de la instalación).
El esqueleto de varios ficheros de entrada para Otter
En estos ejemplo se puede observar:
-----> 5 [binary,4.1,3.1] $F.
que indica que fue posible encontrar una contradicción
(la claúsula vacía o '$F') y Otter finaliza con
el mensaje:
En este enlace se puede ver otro ejemplo más complejo,
que resuelve un puzzle llamado "The
Animals" creado por Lewis Carroll
En cuando a la salida producida por Otter, si el teorema
es válido se puede ver en uno de los ejemplos algo similar a:
That finishes the proof
of the theorem.
Cada línea de la prueba indica el número de
paso en la prueba (5), la regla de
resolución aplicada (binary),
las claúsulas que utilizó y el literal dentro de cada claúsula
(2.1 y 1.1).
using UR-resolution (Unit resulting resolution).
El objetivo concreto de esta práctica es resolver
el problema 3 del examen final 2000 usando Otter.
Defensa de la práctica
La práctica se defenderá en el laboratorio de prácticas
asignado a la asignatura y en las horas de prácticas el día 23 de
Enero de 2003. La defensa consistirá en la entrega de
la solución del problema propuesto acompañada de un dibujo del árbol de prueba, y la solución a otro problema planteado en el momento de la entrega.