Diferencia entre revisiones de «DAO2011 (Demostración asistida por ordenador)»
De Demostración asistida por ordenador (2011-12)
(→Temas y ejercicios) |
|||
| (No se muestran 10 ediciones intermedias del mismo usuario) | |||
| Línea 1: | Línea 1: | ||
| − | + | 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, | |
| − | * | + | * 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. | ||
| − | = Ejercicios | + | 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. | ||
| + | |||
| + | == Razonamiento automático (2011-12) == | ||
| + | * [[Tema 6: Isabelle como un lenguaje funcional]]. | ||
| + | * [[Tema 7: El lenguaje de demostración Isar]]. | ||
| + | * [[Tema 8: Distinción de casos e inducción]]. | ||
| + | * [[Tema 9: Patrones de demostración]]. | ||
| + | * [[Tema 10: Heurísticas para la inducción y recursión general]]. | ||
| + | * [[Tema 11: Caso de estudio: Compilación de expresiones]]. | ||
| + | * [[Tema 12: Conjuntos, funciones y relaciones]]. | ||
Revisión actual del 20:19 15 jul 2018
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.
Razonamiento automático (2011-12)
- Tema 6: Isabelle como un lenguaje funcional.
- Tema 7: El lenguaje de demostración Isar.
- Tema 8: Distinción de casos e inducción.
- Tema 9: Patrones de demostración.
- Tema 10: Heurísticas para la inducción y recursión general.
- Tema 11: Caso de estudio: Compilación de expresiones.
- Tema 12: Conjuntos, funciones y relaciones.