LMF2016: Algoritmo DPLL (Davis, Putnam, Logemann y Loveland)
En la segunda parte de la clase de hoy del curso Lógica matemática y fundamentos hemos estudiado el algoritmo DPLL (Davis, Putnam, Logemann y Loveland) para decidir la consistencia de conjuntos de cláusulas.
En primer lugar se ha explicado el concepto de equiconsistencia. A continuación, las reglas de eliminación de tautologías, de eliminación unitaria, de eliminación de literales puros y la de división. Finalmente, el algoritmo DPLL.
Las transparencias utilizadas son las página 1 a 12 del tema 6.