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

En la primera parte de la clase de hoy del curso Lógica Informática hemos estudiado el algoritmo DPLL (Davis, Putnam, Logemann y Loveland) para decidir la consistencia de conjuntos de cláusulas.

Las transparencias utilizadas son las páginas 1 a 12 del tema 6

En la segunda parte de la clase, se ha comentado la solución del primer ejercicio de la relación 8 y se han dejado como tarea los restantes ejercicios de la relación.