LMF2013: Algoritmo DPLL (Davis, Putnam, Logemann y Loveland)

En la segunda parte de la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) hemos estudiado el algoritmo DPLL (Davis, Putnam, Logemann y Loveland).

Además, se ha comentado la propuesta del 4º ejercicio evaluable consistente en la implementación en Haskell del algoritmo de DPLL y de refinamientos de resolución.

Las transparencias utilizadas son las del tema 6