Tesis profesional presentada por María Enedina Carmona Flores

Maestría en Ciencias con Especialidad en Ingeniería en Sistemas Computacionales. Departamento de Ingeniería en Sistemas Computacionales. Escuela de Ingeniería, Universidad de las Américas Puebla.

Jurado Calificador

Presidente: Dr. Fernando Antonio Aguilera Ramírez
Vocal y Director: Dr. Mauricio Javier Osorio Galindo
Secretario: Dr. Rogelio Dávila Pérez

Cholula, Puebla, México a 17 de mayo de 2000.

Resumen

El razonamiento automático es un área de la Inteligencia Artificial cuyo objetivo es escribir programas de computadora que sirvan de asistencia en la resolución de problemas y en responder preguntas que requieran de razonamiento [ Mir99] . Actualmente existen diferentes programas de razonamiento automático, entre ellos podemos nombrar a: OTTER, ROO, MACE y EQP.

Mediante el razonamiento automático se han obtenido pruebas de resultados que no eran conocidos en matemáticas, es decir, que no...

Resumen (archivo pdf, 36 kb).

Índice de contenido

Agradecimientos (archivo pdf, 35 kb)

Índices (archivo pdf, 49 kb)

Capítulo 1. Introducción al Razonamiento Automático (archivo pdf, 48 kb)

  • 1.1 Un primer acercamiento al Razonamiento Automático
  • 1.2 Alcance de la tesis
  • 1.3 Contenido de la tesis

Capítulo 2. El Método de Resolución (archivo pdf, 139 kb)

  • 2.1 Resolución
  • 2.2 Ejemplo del Método de Resolución
  • 2.3 ¿Qué es un Modelo?
  • 2.4 Algoritmo para transformar una fórmula a su forma clausular [Mal84]
  • 2.5 Ejemplo de transformación de una fórmula a su forma clausular

Capítulo 3. Razonamiento Automático en OTTER (archivo pdf, 113 kb)

  • 3.1 ¿Qué es OTTER?
  • 3.2 Importancia de OTTER
  • 3.3 Aplicaciones relevantes
  • 3.4 Estrategia de razonamiento en OTTER
  • 3.5 Arquitectura de OTTER
  • 3.6 El proceso de Inferencia de OTTER
  • 3.7 Ejemplificación de OTTER

Capítulo 4. La Herramienta Models_WFS (archivo pdf, 148 kb)

  • 4.1 Lenguaje de Representación para Models_WFS
  • 4.2 Definiciones
  • 4.3 Transformaciones aplicadas a Models_WFS
  • 4.4 Criterio de aplicación de Transformaciones
  • 4.5 Mejor Criterio de Aplicación de Transformaciones
  • 4.6 Ejemplificación de Models_WFS
  • 4.7 Solución usando Models_WFS

Capítulo 5. Conclusiones (archivo pdf, 38 kb)

Referencias (archivo pdf, 41 kb)

Apéndice A. Uso de la Herramienta OTTER (archivo pdf, 35 kb)

Apéndice B. Uso de la Herramienta Models_WFS (archivo pdf, 36 kb)

Carmona Flores, M. E. 2000. Constructor de modelos para mejorar el desempeño del razonamiento automático en OTTER. Tesis Maestría. Ciencias con Especialidad en Ingeniería en Sistemas Computacionales. Departamento de Ingeniería en Sistemas Computacionales, Escuela de Ingeniería, Universidad de las Américas Puebla. Mayo. Derechos Reservados © 2000.