DAO2011 (Demostración asistida por ordenador)
De Demostración asistida por ordenador (2011-12)
Este curso es una introducción a la demostración asistida por ordenador usando el sistema Isabelle/HOL/Isar). Los objetivos del curso son:
- desarrollar la capacidad de razonamiento lógico,
- conocer formalismos de representación del conocimiento matemático,
- saber usar sistemas de razonamiento y
- desarrollar teorías matemáticas en sistemas de demostración automática.
Administrativamente, es un curso de formación especializada del Centro de Formación Permanente de la Universidad de Sevilla.
Material para el curso
- Temas: Teorías de los temas.
- Ejercicios: Relaciones de ejercicios.
- Documentación: Enlaces con documentación.
- Sistemas: Sistemas utilizados.
- Diario: Descripción diaria de las clases.
Razonamiento automático (2011-12)
- Tema 6: Isabelle como un lenguaje funcional.
- Tema 7: El lenguaje de demostración 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: Compilación de expresiones.
- Tema 12: Conjuntos, funciones y relaciones.