Diferencia entre revisiones de «DAO2012 (Demostración asistida por ordenador)»
De Demostración asistida por ordenador (2012-13)
(Página creada con '== 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/...') |
(→Material para el curso) |
||
| Línea 8: | Línea 8: | ||
* [[Temas]]: Teorías de los temas. | * [[Temas]]: Teorías de los temas. | ||
* [[Ejercicios]]: Relaciones de ejercicios. | * [[Ejercicios]]: Relaciones de ejercicios. | ||
| − | + | * [http://www.glc.us.es/~jalonso/vestigium/tag/dao2012/ Diario]: Descripción diaria de las clases. | |
| − | |||
| − | * [http://www.glc.us.es/~jalonso/vestigium/tag/ | ||
Revisión del 18:35 20 nov 2012
Demostración asistida por ordenador
Este seminario es una introducción a la demostración asistida por ordenador usando el sistema 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.
- Diario: Descripción diaria de las clases.