Ejercicio 5
De Lógica matemática y fundamentos (2012-13)
Enunciado
El quinto ejercicio evaluable consiste en realizar dos casos de estudio, las expresiones booleanas y las expresiones condicionales. Concretamente:
- Especificación en Haskell de las expresiones booleanaas y de las expresiones condicionales. Funciones que transforman una expresión booleana en una expresión condicional normalizada.
- Demostración de la corrección de la función de transformación, usando Isabelle/HOL.
Los ficheros correspondientes son: (Enunciado en Haskell y Enunciado en Isabelle/HOL).
Los ficheros con las soluciones (usuario_5.hs y usuario_5.thy) se enviarán a mjoseh@us.es antes del lunes 17 de junio.