LMF2016: Formas normales de Skolem y cláusulas

En la primera parte de la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo 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 continuación se ha estudiado la sintaxis y la semántica de la lógica clausal de primer orden.

Mediante las formas de Skolem, se obtien un algoritmo que dado un conjunto S de fórmulas de primer orden obtiene un conjunto de cláusulas S’ tal que S y S’ son equiconsistentes. De esta forma, el problema de consecuencia en la lógica de primer orden se reduce al de consistencia de un conjunto de cláusulas.

Las transparencias usadas son las del tema 10.