Ver código fuente

= 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.

== [http://www.us.es/estudios/master/master_M095/asignatura_50950005 Programa de la asignatura] ==

== [http://www.cs.us.es/~jalonso/cursos/m-ra Página Web] ==