Diferencia entre revisiones de «Temas LCyTM 2015»
De Demostración automática de teoremas (2014-15)
(Página creada con '== Temas de ''Lógica computacional y teoría de modelos (2015-16)'' == *[http://www.cs.us.es/~mjoseh/dat-15/tema-1.pdf Tema 1: Sintaxis y semántica de la Lógica proposicional...') |
|||
| (No se muestran 7 ediciones intermedias del mismo usuario) | |||
| Línea 12: | Línea 12: | ||
* [[Tema 11: Métodos de demostración.]][http://www.cs.us.es/~mjoseh/dat-15/T11.thy] | * [[Tema 11: Métodos de demostración.]][http://www.cs.us.es/~mjoseh/dat-15/T11.thy] | ||
* [[Tema 12: Definiciones inductivas en Isabelle/HOL. Caso de estudio: clausura reflexiva transitiva.]][http://www.cs.us.es/~mjoseh/dat-15/T12.thy] | * [[Tema 12: Definiciones inductivas en Isabelle/HOL. Caso de estudio: clausura reflexiva transitiva.]][http://www.cs.us.es/~mjoseh/dat-15/T12.thy] | ||
| + | * Casos de estudio: | ||
| + | ** [[Tema 13: Expresiones aritméticas.]][http://www.cs.us.es/~mjoseh/LCyTM-15/Hoare/AExp_b.thy] | ||
| + | ** [[Tema 14: Expresiones booleanas.]][http://www.cs.us.es/~mjoseh/LCyTM-15/Hoare/BExp_b.thy] | ||
| + | ** [[Tema 15: Sintaxis de un lenguaje imperativo simple.]][http://www.cs.us.es/~mjoseh/LCyTM-15/Hoare/Com_b.thy] | ||
| + | ** [[Tema 16: Semántica operacional del lenguaje imperativo simple IMP.]][http://www.cs.us.es/~mjoseh/LCyTM-15/Hoare/Big_Step_b.thy] | ||
| + | ** [[Tema 17: Lógica de Hoare en Isabelle/HOL.]][http://www.cs.us.es/~mjoseh/LCyTM-15/Hoare/Hoare_b.thy] | ||
| + | ** [[Ejemplos de verificación de propiedades en Lógica de Hoare usando Isabelle/HOL.]][http://www.cs.us.es/~mjoseh/LCyTM-15/Hoare/Hoare_b_ejemplos.thy] | ||
| + | ** [[Tema 18: Adecuación y completitud de la Lógica de Hoare en Isabelle/HOL.]][http://www.cs.us.es/~mjoseh/LCyTM-15/Hoare/Hoare_Sound_Complete_b.thy] | ||
| + | ** [[Tema 19: Lógica de Hoare en Isabelle/HOL: adecuación y completitud de la corrección total.]][http://www.cs.us.es/~mjoseh/LCyTM-15/Hoare/Hoare_Total_b.thy] | ||
| + | ** [[Tema 20: Lógica de Hoare en Isabelle/HOL: condiciones de verificación.]][http://www.cs.us.es/~mjoseh/LCyTM-15/Hoare/VCG_b.thy] | ||
| + | <!-- | ||
* [[Tema 13: Razonamiento modular (I): Teoría de grupos.]][http://www.cs.us.es/~mjoseh/dat-15/T13.thy] | * [[Tema 13: Razonamiento modular (I): Teoría de grupos.]][http://www.cs.us.es/~mjoseh/dat-15/T13.thy] | ||
* [[Tema 14: Razonamiento modular (II): Órdenes y retículos.]][http://www.cs.us.es/~mjoseh/dat-15/T14.thy] | * [[Tema 14: Razonamiento modular (II): Órdenes y retículos.]][http://www.cs.us.es/~mjoseh/dat-15/T14.thy] | ||
| Línea 18: | Línea 29: | ||
** [[Tema 15(b): sustitución de definiciones.]][http://www.cs.us.es/~mjoseh/dat-15/T15b.thy] | ** [[Tema 15(b): sustitución de definiciones.]][http://www.cs.us.es/~mjoseh/dat-15/T15b.thy] | ||
** [[Tema 15(c): interpretaciones locales.]][http://www.cs.us.es/~mjoseh/dat-15/T15c.thy] | ** [[Tema 15(c): interpretaciones locales.]][http://www.cs.us.es/~mjoseh/dat-15/T15c.thy] | ||
| + | --> | ||
Revisión actual del 20:12 8 feb 2016
Temas de Lógica computacional y teoría de modelos (2015-16)
- Tema 1: Sintaxis y semántica de la Lógica proposicional.
- Tema 2: Deducción natural en Lógica proposicional.
- Tema 3: Deducción natural en Lógica proposicional con Isabelle/HOL.[1]
- Tema 4: Sintaxis y semántica de la Lógica de primer orden.
- Tema 5: Deducción natural en Lógica de primer orden.
- Tema 6: Deducción natural en Lógica de primer orden con Isabelle/HOL.[2]
- Tema 7: Programación funcional en Isabelle/HOL.[3]
- Tema 8: Razonamiento sobre programas en Isabelle/HOL.[4]
- Tema 9: Razonamiento por casos e inducción.[5]
- Tema 10: Conjuntos, funciones y relaciones.[6]
- Tema 11: Métodos de demostración.[7]
- Tema 12: Definiciones inductivas en Isabelle/HOL. Caso de estudio: clausura reflexiva transitiva.[8]
- Casos de estudio:
- Tema 13: Expresiones aritméticas.[9]
- Tema 14: Expresiones booleanas.[10]
- Tema 15: Sintaxis de un lenguaje imperativo simple.[11]
- Tema 16: Semántica operacional del lenguaje imperativo simple IMP.[12]
- Tema 17: Lógica de Hoare en Isabelle/HOL.[13]
- Ejemplos de verificación de propiedades en Lógica de Hoare usando Isabelle/HOL.[14]
- Tema 18: Adecuación y completitud de la Lógica de Hoare en Isabelle/HOL.[15]
- Tema 19: Lógica de Hoare en Isabelle/HOL: adecuación y completitud de la corrección total.[16]
- Tema 20: Lógica de Hoare en Isabelle/HOL: condiciones de verificación.[17]