Acciones

Diferencia entre revisiones de «Ejercicio 4»

De Lógica matemática y fundamentos (2012-13)

 
(No se muestran 2 ediciones intermedias del mismo usuario)
Línea 3: Línea 3:
 
continuación:
 
continuación:
  
* Programación en Haskell de algunos de los refinamientos de resolución en
+
* 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.
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.  
* 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
 
En ambos casos hay que usar la representación de la lógica proposicional en

Revisión actual del 12:30 15 may 2013

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.