Diferencia entre revisiones de «Temas»
De Demostración automática de teoremas (2014-15)
| 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 artiméticas.]][http://www.cs.us.es/~mjoseh/LCyTM-15/temas/Hoare/AExp_b.thy] | ||
| + | ** [[Tema 14: Expresiones booleanas.]][http://www.cs.us.es/~mjoseh/LCyTM-15/temas/Hoare/BExp_b.thy] | ||
<!-- | <!-- | ||
Revisión del 13:30 5 ene 2016
Temas de Demostración automática de teoremas (2014-15)
- 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: