Ver el código de «DAO2011 (Demostración asistida por ordenador)» - Demostración asistida por ordenador (2011-12)

Este curso es una introducción a la demostración asistida por ordenador usando el sistema [http://www.cl.cam.ac.uk/research/hvg/Isabelle 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 [http://www.cfp.us.es/web/ficha_avanzada.asp?id_titulo=846&tipo=FE&basica=1&curso=2010 curso de formación especializada] del [http://www.cfp.us.es/ Centro de Formación Permanente de la Universidad de Sevilla].

== Material para el curso ==
* [[Temas]]: Teorías de los temas.
* [[Ejercicios]]: Relaciones de ejercicios.
* [http://www.cs.us.es/~jalonso/cursos/dao/doc.html Documentación]: Enlaces con documentación.
* [http://www.cs.us.es/~jalonso/cursos/dao/sistemas.html Sistemas]: Sistemas utilizados.
* [http://www.glc.us.es/~jalonso/vestigium/tag/dao2011/ 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]].