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, y para ello es suficiente con disponer del ejecutable de Otter:
Otter - Ejecutable para Solaris
Los fuentes de Otter, manuales, versiones reducidas para Mac y Windows y bibliografía sobre sistemas de deducción automática y sobre los resultados en investigació matemática obtenidos por Otter pueden encontrarse en las paginas web de Otter:
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:
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).
En este enlace se puede ver otro ejemplo más complejo,
que resuelve un puzzle llamado "The
Animals" creado por Lewis Carroll
using UR-resolution (Unit resulting resolution).