Temas de "Razonamiento automático (2010-11)"

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

Presentación del razonamiento automático

• Presentación del razonamiento automático.

Razonamiento asistido con Isabelle/HOL/Isar

Los apuntes se encuentran en Introducción a la demostración asistida por ordenador (con Isabelle/Isar).

El código de los apuntes y todas las teorias se enecuentra en teorias.tgz.

Los temas son los siguientes:

• Tema 1: Isabelle como un lenguaje funcional
  (apuntes y código).
• Tema 2: El lenguaje de demostracion Isar
  (apuntes y código).
• Tema 3: Distinción de casos e inducción
  (apuntes y código).
• Tema 4: Patrones de demostración
  (apuntes y código).
• Tema 5: Heurísticas para la inducción y recursión general
  (apuntes y código).
• Tema 6: Caso de estudio: Corrección de un compilador
  (apuntes y código).
• Tema 7: Conjuntos, funciones y relaciones
  (apuntes y código).
• Tema 8: Misceláneas.
  (código).

[ Inicial | Temas | Ejercicios | Documentación | Sistemas ]