LI2011-12: Formas normales de Skolem y cláusulas

En la clase de hoy del curso Lógica Informática se estudiado cómo se puede diseñar un procedimiento de forma que dada una fórmula F obtenga otra sin cuantificadores G que sea equisatisfacible (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.

Las transparencias de esta clase son las del tema 9