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