Ejercicio 4
De Lógica matemática y fundamentos (2012-13)
Enunciado
El cuarto ejercicio evaluable consiste una de las dos opciones que se ofrecen a continuación:
- Programación en Haskell de algunos de los refinamientos de resolución en lógica proposicional. Las funciones finales han de ser (esValidaPorResolucion* f) para determinar la validez de la fórmula f; y (esConsecuenciaPoResolucion* s f) que determine si la fórmula f es consecuencia lógica del conjunto s, siendo * el refinamiento correspondiente. Esta opción tendrá peso 4 en el cálculo de la calificación por curso.
- Programación en Haskell del algoritmo de Davis-Putnam. Las funciones finales han de ser (esValidaPorDP f) para determinar la validez de la fórmula f; y (esConsecuenciaPorDP s f) que determine si la fórmula f es consecuencia lógica del conjunto s. Esta opción tendrá peso 5 en el cálculo de la calificación por curso.
En ambos casos hay que usar la representación de la lógica proposicional en Haskell, realizada en las relaciones de ejercicios 2, 9 y 10. Se valorará la estructura y la eficiencia de las funciones, así como la claridad de los comentarios.
Se enviará a mjoseh@us.es antes del viernes 31 de mayo de 2013 un fichero usuario_4a.hs o usuario_4b.hs, según la opción elegida.