Ejercicio 4

El cuarto ejercicio evaluable consiste una de las dos opciones que se ofrecen a continuación:

1.- 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.

2.- 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.