Ver el código de «DAO2012 (Demostración asistida por ordenador)» - Demostración asistida por ordenador (2012-13)

== Demostración asistida por ordenador ==
Este seminario 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]). Sus objetivos son:
* desarrollar la capacidad de razonamiento lógico,
* saber usar sistemas de razonamiento y
* desarrollar teorías matemáticas en sistemas de demostración automática. 

== Material para el curso ==
* [[Temas]]: Teorías de los temas.
* [[Ejercicios]]: Relaciones de ejercicios.
* [[Documentación]]: Lecturas recomendadas.
* [http://www.glc.us.es/~jalonso/vestigium/tag/dao2012/ Diario]: Descripción diaria de las clases.