Temas de "Razonamiento automático (2008-09)"

En esta página se encuentra las transparencias de las clases. Están en formato pdf.

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.

[ Inicial | Temas | Documentación | Sistemas ]