LI2015: Formas normales de Skolem y cláusulas
En la primera parte de la clase de hoy del curso de Lógica Informática se estudiado cómo se puede diseñar un procedimiento de forma que dada una fórmula F obtenga otra G que sólo tenga cuantificadores al principio, que su cuerpo esté en forma normal conjuntiva y que sea equisatisfacible con F (es decir, que G es satisfacible precisamente si lo es F). Con dicho procedimiento se calcula la forma normal de Skolem. A partir de las formas se Skolem se obtienen las formas clausales.
En la segunda parte se han comentado las soluciones de los ejercicios 8.5.1 y 8.5.5 del libro de ejercicios. Se han realizado las demostraciones por deducción natural y también por tableros semánticos. Además, se ha comprobado con tableros semánticos la validez de sus recíprocos.
Las transparencias de esta clase son las del tema 10