Todas las páginas
- Demostración automática de teoremas (2014-15)
- Documentación
- Ejemplos de verificación de propiedades en Lógica de Hoare usando Isabelle/HOL.
- Ejercicios
- Página Principal
- R1
- R2
- R3
- R4
- R5
- R6
- R7
- R8
- Rel 1
- Rel 10
- Rel 10 (e)
- Rel 11
- Rel 11 (e)
- Rel 12
- Rel 12 (e)
- Rel 2
- Rel 3
- Rel 4
- Rel 5
- Rel 6
- Rel 7
- Rel 8
- Rel 8 (e)
- Rel 9
- Rel 9 (e)
- Relación 1
- Relación 2
- Relación 3
- Relación 4
- Relación 5
- Relación 6
- Relación 7
- Relación 8
- Sistemas
- T1 1
- T1 2
- T1 3
- Tema 10: Conjuntos, funciones y relaciones.
- Tema 11: Métodos de demostración.
- Tema 12: Definiciones inductivas en Isabelle/HOL. Caso de estudio: clausura reflexiva transitiva.
- Tema 13: Expresiones aritméticas.
- Tema 13: Razonamiento modular (I): Teoría de grupos.
- Tema 14: Expresiones booleanas.
- Tema 14: Razonamiento modular (II): Órdenes y retículos.
- Tema 15(a)
- Tema 15(a): sustitución de parámetros.
- Tema 15(b)
- Tema 15(b): sustitución de definiciones.
- Tema 15(c)
- Tema 15(c): interpretaciones locales.
- Tema 15: Sintaxis de un lenguaje imperativo simple.
- Tema 16: Semántica operacional del lenguaje imperativo simple IMP.
- Tema 17: Lógica de Hoare en Isabelle/HOL.
- Tema 18: Adecuación y completitud de la Lógica de Hoare en Isabelle/HOL.
- Tema 19: Lógica de Hoare en Isabelle/HOL: adecuación y completitud de la corrección total.
- Tema 20: Lógica de Hoare en Isabelle/HOL: condiciones de verificación.
- Tema 3: Deducción natural en Lógica proposicional con Isabelle/HOL
- Tema 6: Deducción natural en Lógica de primer orden con Isabelle/HOL
- Tema 7: Programación funcional en Isabelle/HOL.
- Tema 8: Razonamiento sobre programas en Isabelle/HOL.
- Tema 9: Razonamiento por casos e inducción.
- Temas
- Temas LCyTM 2015
- Trabajos