Diferencia entre revisiones de «DAO2011 (Demostración asistida por ordenador)»
De Demostración asistida por ordenador (2011-12)
(→Demostración asistida por ordenador (2011)) |
|||
| Línea 1: | Línea 1: | ||
| − | = Demostración asistida por ordenador | + | == Demostración asistida por ordenador == |
| − | |||
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: | 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, | * desarrollar la capacidad de razonamiento lógico, | ||
Revisión del 23:04 1 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.