Diferencia entre revisiones de «DAO2011 (Demostración asistida por ordenador)»
De Demostración asistida por ordenador (2011-12)
m (Protegió «DAO2011 (Demostración asistida por ordenador)» ([edit=sysop] (indefinido) [move=sysop] (indefinido))) |
(→Material para el curso) |
||
Línea 11: | Línea 11: | ||
* [[Temas]]: Teorías de los temas. | * [[Temas]]: Teorías de los temas. | ||
* [[Ejercicios]]: Relaciones de ejercicios. | * [[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/doc.html Documentación]: Enlaces con documentación. |
* [http://www.cs.us.es/~jalonso/cursos/dao/sistemas.html Sistemas]: Sistemas utilizados. | * [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. | * [http://www.glc.us.es/~jalonso/vestigium/tag/dao2011/ Diario]: Descripción diaria de las clases. |
Revisión del 18:25 8 mar 2011
Demostración asistida por ordenador
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.