Revisión del 23:03 1 mar 2011

Demostración asistida por ordenador (2011)

Este curso es una introducción a la demostración asistida por ordenador usando el sistema Isabelle/HOL/Isar). Los objetivos del curso son:

@@ Línea 1: / Línea 1: @@
-= Temas =
+= Demostración asistida por ordenador (2011) =
-* [[Tema 1: Isabelle como un lenguaje funcional]].
-* [[Tema 2: Razonamiento sobre programas]].
-= Ejercicios =
+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:
-* '''Relación 1:''' Razonamiento sobre programas ([[Rel_1|Enunciado]] y [[Relación 1|Solución colaborativa]]).
+* 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.