Razonamiento Automático

Bloque 0: Introducción

Tema 0: Introducción a los sistemas de razonamiento automático

Bloque 1: El sistema de razonamiento automático OTTER

Tema 1: Introducción
Ejemplos: fichas.in, grupos.in, componente-or.in.
Tema 2: Resolución de primer orden
Tema 3: Tratamiento de la igualdad
Tema 4: Predicados evaluables

Bloque 2: El sistema de razonamiento automático ACL2

Tema 1: Introducción
Tema 2: Recursión e inducción
Tema 3: Reescritura
Tema 4: Interacción con el sistema

Bloque 3: El sistema de razonamiento automático NuSMV (Desde el curso 2009/2010)

Tema 1: Introducción
Tema 2: Lógicas temporales
Tema 3: Verificación basada en modelos (Model Checking)
Tema 4: Interacción con el sistema

Bloque 4: El sistema de razonamiento automático PVS (Hasta el curso 2008/2009)

Tema 1: Introducción
Tema 2: Lógica y teorías de primer orden
Tema 3: Aritmética e inducción
Tema 4: Tipos abstractos de datos