Diferencia entre revisiones de «Temas»
De DAO (Demostración asistida por ordenador)
(→Temas de Demostración asistida por ordenador) |
(→Temas de Demostración asistida por ordenador) |
||
| (No se muestran 12 ediciones intermedias del mismo usuario) | |||
| Línea 1: | Línea 1: | ||
== Temas de ''Demostración asistida por ordenador'' == | == Temas de ''Demostración asistida por ordenador'' == | ||
| − | * [[Tema | + | * [[Tema 1: Deducción natural proposicional con Isabelle/HOL]]. |
| − | + | * [[Tema 2: Deducción natural en lógica de primer orden en Isabelle/HOL]]. | |
| − | + | * [[Tema 3: Resumen del lenguaje Isabelle/Isar y las reglas de la lógica]]. | |
| − | * [[Tema | + | * [[Tema 4: Programación funcional en Isabelle]]. |
| − | * [[Tema | + | * [[Tema 5: Razonamiento sobre programas]]. |
* [[Tema 6: Razonamiento por casos y por inducción en Isabelle/HOL]]. | * [[Tema 6: Razonamiento por casos y por inducción en Isabelle/HOL]]. | ||
| + | * [[Tema 7: Caso de estudio: Compilacion de expresiones]]. | ||
| + | * [[Tema 8: Conjuntos, funciones y relaciones]]. | ||
| + | * [http://www.cs.us.es/~jalonso/cursos/dao-12/temas/tema-1.pdf Tema 9: Panorama de la demostración asistida por ordenador]. | ||
Revisión actual del 09:07 20 jun 2013
Temas de Demostración asistida por ordenador
- Tema 1: Deducción natural proposicional con Isabelle/HOL.
- Tema 2: Deducción natural en lógica de primer orden en Isabelle/HOL.
- Tema 3: Resumen del lenguaje Isabelle/Isar y las reglas de la lógica.
- Tema 4: Programación funcional en Isabelle.
- Tema 5: Razonamiento sobre programas.
- Tema 6: Razonamiento por casos y por inducción en Isabelle/HOL.
- Tema 7: Caso de estudio: Compilacion de expresiones.
- Tema 8: Conjuntos, funciones y relaciones.
- Tema 9: Panorama de la demostración asistida por ordenador.