modified on 21 feb 2013 at 02:28 ••• 5.668 views

Razonamiento Automático

De Master

Contenido

El objetivo del curso es la presentación de las técnicas usadas en la representación del conocimiento y a los métodos de razonamiento automático asociados. En el curso se estudia la representación del conocimiento mediante la lógica, el uso de representaciones como base para el razonamiento y procesos de razonamiento para obtener los objetivos. El contenido es el siguiente:

Parte 1: Introducción

  • Tema 0: Introducción al razonamiento automático.
  • Tema 1: Lógica de primer orden.

Parte 2: Razonamiento automático por resolución con OTTER y MACE

  • Tema 2: Razonamiento proposicional con OTTER y MACE.
  • Tema 3: Razonamiento de primer orden con OTTER y MACE.
  • Tema 4: Razonamiento ecuacional con OTTER.

Parte 3: Razonamiento asistido con Isabelle/HOL/Isar

  • Tema 6: Isabelle como un lenguaje funcional.
  • Tema 7: El lenguaje de demostracion Isar.
  • Tema 8: Distinción de casos e inducción.
  • Tema 9: Patrones de demostración.
  • Tema 10: Heurísticas para la inducción y recursión general.
  • Tema 11: Caso de estudio: Corrección de un compilador.
  • Tema 12: Conjuntos, funciones y relaciones.

Programa de la asignatura

Página Web