LI2015: 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.
En la segunda parte, se ha explicado la solución del 3º ejercicio del primer examen del curso 2014-15:
Decidir, mediante tableros semánticos, si la fórmula
- p → q ∨ s
es consecuencia lógica del conjunto de fórmulas
- {q → s, ¬(¬p ∧ q)}.
En el caso de que no lo sea, dar un contramodelo.
Las transparencias utilizadas son las las página 1 a 12 del tema 6