Otter

OTTER

Inteligencia Artificial I
Curso 2005/2006
Claudia Bernardos Gómez
Sara García Solano
Berta Mª Pérez Esteban
María Pérez León

OTTER

2

Introducción ............................................................................................................ 3
1.1. ¿Qué es OTTER? ............................................................................................ 31.2. Razonamiento Automático ............................................................................ 3
2. El proceso de inferencia en OTTER: ciclo de trabajo ........................................ 4
2.1. Estrategias de razonamiento en OTTER...................................................... 4
2.2. Ciclo detrabajo............................................................................................... 4
3. Reglas de inferencia adicionales: hiperresolución y paramodulación ............... 6
3.1. Hiperresolución............................................................................................... 6
3.2. Paramodulación .............................................................................................. 8
4. Estrategias adicionales: demodulación yasignación de pesos .......................... 10
4.1. Demodulación ............................................................................................... 10
4.2. Asignación de pesos ...................................................................................... 12
5. Ejemplos de aplicación: ....................................................................................... 135.1. Búsqueda en espacio de estados .................................................................. 13
5.2. Simplificación de polinomios ....................................................................... 17
5.3. Puzzles ........................................................................................................... 23
6. Apéndice................................................................................................................ 29
7. Bibliografía ............................................................................................................ 31
1.

OTTER

3

1. Introducción
1.1. ¿Qué es OTTER?
OTTER (Organized Techniques For Theorem-Proving And Effective Research),
es un sistema de razonamiento automático que implementa el método deresolución para la lógica de primer orden con igualdad. Usa una sintaxis similar
a la de Prolog.
Es un demostrador por refutación, esto es, busca una contradicción a partir de un
conjunto de fórmulas. OTTER no sirve para solucionar problemas de teoría de
números, cálculo, geometría plana, y verificación de Hardware. Esto se debe a
que requiere de inducción y funciones de alto nivel. Para loque sí sirve es para
aplicaciones de álgebra abstracta, lógica formal, lógica combinatoria y álgebras
booleanas.
Fue desarrollado por William McCune en el Departamento de Matemáticas y
Ciencias de la Computación del “Argonne National Laboratory”, en 1988.

1.2. Razonamiento Automático
El razonamiento automático se dedica a estudiar cómo usar un ordenador para
resolver problemas querequieren razonamiento. Algunos problemas que surgen
durante dicho estudio son la representación del reconocimiento, las reglas para
derivar nuevo conocimiento del que se tiene, y las estrategias para controlar
dichas reglas. Otras cuestiones se refieren a la implementación de la teoría
resultante y a las aplicaciones para las cuales el correspondiente software puede
ser usado. La teoría,implementación y aplicaciones, son vitales para el
razonamiento automático a la hora de proporcionar un asistente de razonamiento
automático
El razonamiento automático se dedica al desarrollo de programas de ordenador
que sean capaces de demostrar que una conjetura es una consecuencia lógica de
un conjunto de axiomas o hipótesis. El lenguaje en el que la conjetura, las
hipótesis, y los axiomas son...