Lógica Computacional
Nota 10. Formas normales para la lógica de predicados

1 Introducción

La regla de resolución es una regla de inferencia para la lógica de predicados análoga a de la lógica proposicional. Tal regla funciona únicamente sobre expresiones en forma clausular.

2 FNCP y Forma Clausular

Ocuparemos la noción de literal que se introdujo en la nota pasada.

Definición 2.1.

Una expresión está en forma normal conjuntiva syss es una conjunción de disyunciones de literales.

La forma normal conjuntiva se utilizó de forma implícita para obtener la forma clausular en la lógica proposicional.

Definición 2.2.

Una fórmula de la lógica de predicados está en forma normal conjuntiva prenex (FNCP) syss es de la forma:

$$Q_1{x}_1\mathrm{\cdots }{Q}_n{x}_{n}M$$

donde las $Q_i$ son cuantificadores y $M$ es una fórmula libre de cuantificadores en forma normal conjuntiva. A la secuencia $Q_1{x}_1\mathrm{\cdots }{Q}_n{x}_n$ se le conoce como prefijo y a $M$ como matriz.

Definición 2.3.

Sea $\phi$ un enunciado, es decir, una fórmula cerrada, en FNCP cuyo prefijo consiste únicamente de cuantificadores universales. La forma clausular de $\phi$ consiste en la matriz de $\phi$ escrita como un conjunto de cláusulas.

Definición 2.4.

Sean $\phi$ y $\psi$ dos fórmulas de la lógica de predicados. La expresión $\phi \approx \psi$ denota que $\phi$ es satisfacible syss $\psi$ es satisfacible.

Es importante entender que $\phi \approx \psi$ ($\phi$ es satisfacible syss $\psi$ es satisfacible) no implica que $\phi \equiv \psi$ ($\phi$ es lógicamente equivalente a $\psi$). Por un lado, $\phi \approx \psi$ indica que existe un modelo para $\phi$ syss existe un modelo para $\psi$. Por otro lado, la equivalencia lógica $\phi \equiv \psi$ quiere decir que todo modelo $ℳ$ satisface a $\phi$ syss también satisface a $\psi$.

Teorema 2.5 (Skolem).

Sea $\phi$ una fórmula cerrada. Entonces existe una fórmula $\psi$ en forma clausular tal que $\phi \approx \psi$.

Es claro que podemos transformar la $\phi$ del Teorema 2.5 en una fórmula lógicamente equivalente en FNCP. Es la eliminación de los cuantificadores existenciales lo que causa que la nueva fórmula no sea equivalente a la original. Esta eliminación se consigue definiendo nuevos símbolos de función. En $\forall x\exists yP(x,y)$, los cuantificadores pueden leerse de la siguiente manera: todo $x$ produce un valor asociado $y$ tal que el predicado $P$ es verdadero. Pero nuestro concepto intuitivo de una función es el mismo: $y=f(x)$ significa que, dado $x$, $f$ produce un valor $y$ asociado con $x$. El cuantificador existencial puede eliminarse, resultando en $\forall xP(x,f(x))$.

Ejemplo 2.6.

Consideremos el modelo $ℳ$ para la fórmula en FNCP $\phi =\forall x\exists yP(x,y)$, donde el universo es $\mathbb{Z}$ y el predicado $P^{ℳ}\stackrel{def}{=}>$. Obviamente, $ℳ\vDash \phi$.

La fórmula ${\phi }^{\prime }=\forall xP(x,f(x))$ se obtiene a partir de $\phi$ eliminando el cuantificador existencial y reemplazándolo por una función. Consideremos el modelo ${ℳ}^{\prime }$ idéntico a $ℳ$ pero con $f^{{ℳ}^{\prime }}(x)\stackrel{def}{=}x+1$. Claramente, ${ℳ}^{\prime }\vDash \phi$ (simplemente se ignora la función), pero ${ℳ}^{\prime }\vDash ̸{\phi }^{\prime }$ ya que no es cierto que $n>n+1$ para los enteros. Por lo tanto, ${\phi }^{\prime }\not\equiv \phi$.

Sin embargo, sí existe un modelo para ${\phi }^{\prime }$, por ejemplo ${ℳ}^{\star }$, donde el universo es $\mathbb{Z}$, $P^{{ℳ}^{\star }}\stackrel{def}{=}>$ y $f^{{ℳ}^{\star }}(x)\stackrel{def}{=}x-1$.

3 Algoritmo de Skolem

Damos ahora un algoritmo para transformar una fórmula de la lógica de predicados $\phi$ en una fórmula $\psi$ en forma clausular.

Algoritmo

Input: Una fórmula cerrada $\phi$ de la lógica de predicados.

Output: Una fórmula $\psi$ en forma clausular tal que $\phi \approx \psi$.

Daremos los pasos del algoritmo a la par que lo aplicamos a la fórmula

$$▲\phi =\forall x\left(P(x)\to Q(x)\right)\to \left(\forall xP(x)\to \forall xQ(x)\right)$$

1. Se limpia la fórmula de entrada $\phi$.

   • Eliminar cuantificadores múltiples mediante las siguientes equivalencias:

     $$\begin{array}{ccc}\forall x\forall x\phi \equiv \forall x\phi & & \\ \exists x\exists x\phi \equiv \exists x\phi & & \end{array}$$

     $$\begin{array}{ccc}\exists x\forall x\phi \equiv \forall x\phi & & \\ \forall x\exists x\phi \equiv \exists x\phi & & \end{array}$$

   • Eliminar los cuantificadores vacuos mediante las siguientes equivalencias, donde $x$ no está libre en $\phi$:

     $$\forall x\phi \equiv \phi$$

     $$\exists x\phi \equiv \phi$$

   $▲$No es necesaria hacer ninguna transformación a la fórmula $\phi$.

2. Eliminar las implicaciones y bi-condicionales empleando las equivalencias:

   $▲\neg \forall x\left(\neg P(x)\vee Q(x)\right)\vee \left(\neg \forall xP(x)\vee \forall xQ(x)\right)$

3. Manipular la negación para permitir su efecto únicamente en fórmulas atómicas y quitar doble negaciones. Usar las siguientes equivalencias:

   $▲\exists x\left(P(x)\wedge \neg Q(x)\right)\vee \left(\exists x\neg P(x)\vee \forall xQ(x)\right)$

4. Renombrar variables ligadas para que ninguna variable se repita en los cuantificadores.

   $▲\exists x\left(P(x)\wedge \neg Q(x)\right)\vee \left(\exists y\neg P(y)\vee \forall zQ(z)\right)$

5. Extraer cuantificadores de la matriz. Identificar un cuantificador más externo en la matriz, es decir, uno que no esté dentro del alcance de otro que también resida en la matriz, y extraerlo usando las siguientes equivalencias, donde $Q$ es un cuantificador y $op$ es $\vee$ o $\wedge$:

   $$\psi opQx\phi \equiv Qx(\psi op\phi )$$

   $$Qx\phi op\psi \equiv Qx(\phi op\psi )$$

   Repetir hasta que todos los cuantificadores aparezcan en el prefijo y ninguno en la matriz. Las equivalencias se pueden aplicar porque ninguna variable figura en dos o más cuantificadores.

   $▲\exists x\exists y\forall z\left(\left(P(x)\wedge \neg Q(x)\right)\vee \left(\neg P(y)\vee Q(z)\right)\right)$

6. Usar las leyes distributivas para transformar la matriz a su FNC. La fórmula está ahora en FNCP.

   $▲\exists x\exists y\forall z\left(\left(P(x)\vee \neg P(y)\vee Q(z)\right)\wedge \left(\neg Q(x)\vee \neg P(y)\vee Q(z)\right)\right)$

7. Recorrer el prefijo de izquierda a derecha. Para todo cuantificador existencial $\exists x$ en $\phi$, sean $y_1,\mathrm{\dots }{y}_n$ las variables cuantificadas universalmente que preceden a $\exists x$, y sea $f$ un nuevo símbolo de función de aridad $n$. Eliminar $\exists x$ y reemplazar en la matriz cada presencia de $x$ por $f(y_1,\mathrm{\dots }{y}_n)$, esta función se llama función de Skolem. Si no hay cuantificadores universales precediendo $\exists x$, reemplazar $x$ por una nueva constante, la cual se llama constante de Skolem. El proceso de reemplazar cuantificadores existenciales por funciones se llama Skolemización.

   $▲\forall z\left(\left(P(a)\vee \neg P(b)\vee Q(z)\right)\wedge \left(\neg Q(a)\vee \neg P(b)\vee Q(z)\right)\right)$

8. La fórmula puede ser escrita en forma clausular al dejar a un lado los cuantificadores universales y al escribir la matriz como un conjunto de cláusulas.

   $$\{\{P(a),\neg P(b),Q(z)\},\{\neg Q(a),\neg P(b),Q(z)\}\}$$

Para recordar los pasos LINREDS pueden pensar en la frase:

• Logic Is Necessary in Realizing Effective Durable Systems (La lógica es necesaria en la realización de sistemas efectivos y durables).

Si buscan una frase en español se tiene la siguiente:

• La INformática REvoluciona el Desarrollo de Sociedades.

Notemos que el orden en el que se extraen los cuantificadores en el paso E puede ser otro, y una vez aplicadas las leyes distributivas obtenemos la siguiente fórmula en FNCP equivalente:

$$\forall z\exists x\exists y\left(\left(P(x)\vee \neg P(y)\vee Q(z)\right)\wedge \left(\neg Q(x)\vee \neg P(y)\vee Q(z)\right)\right)$$

Como los cuantificadores existenciales están precedidos por un cuantificador universal, la Skolemización produce funciones de un argumento, no constantes, como sigue:

$$\forall z\left(\left(P(f(z))\vee \neg P(g(z))\vee Q(z)\right)\wedge \left(\neg Q(f(z))\vee \neg P(g(z))\vee Q(z)\right)\right)$$

En forma clausular tenemos:

$$\{\{P(f(z)),\neg P(g(z)),Q(z)\},\{\neg Q(f(z)),\neg P(g(z)),Q(z)\}\}$$

3.1 Demostración del algoritmo de Skolem

En el algoritmo anterior se emplean cinco equivalencias, es el remplazo de un cuantificador existencial por una función/constante de Skolem lo que ya las hace equivalentes, pero la satisfacibilidad se preserva. Suponga que:

$$ℳ\vDash \forall y_1\mathrm{\dots }\forall y_n\exists xP(y_1,\mathrm{\dots },y_n,x).$$

Necesitamos demostrar que existe un modelo ${ℳ}^{\prime }$ tal que:

$${ℳ}^{\prime }\vDash \forall y_1\mathrm{\dots }\forall y_{n}P(y_1,\mathrm{\dots },y_n,f(y_1,\mathrm{\dots },y_n)).$$

${ℳ}^{\prime }$ se construye extendiendo $ℳ$. Se agrega una función $f^{(n)}$ definida para todo $\{c_1,\mathrm{\dots },c_n\}\subseteq A$ como:

$$f(c_1,\mathrm{\dots },c_n)=c_{n+1}\text{ para algún }{c}_{n+1}\in A\text{, tal que }(c_1,\mathrm{\dots },c_n,c_{n+1})\in P^{ℳ}.$$

Dado que $ℳ\vDash \forall y_1\mathrm{\dots }\forall y_n\exists xP(y_1,\mathrm{\dots },y_n,x)$, debe haber al menos un elemento $b$ en el dominio tal que $(c_1,\mathrm{\dots },c_n,b)\in P^{ℳ}$. Simplemente elegimos uno de ellos arbitrariamente y lo asignamos como el valor $c_{n+1}$ de $f(c_1,\mathrm{\dots },c_n)$. La función de Skolem se elige como un nuevo símbolo de función, por lo que la definición de $f$ no entra en conflicto con ninguna función existente en $ℳ$.

Para demostrar que:

$${ℳ}^{\prime }\vDash \forall y_1\mathrm{\dots }\forall y_{n}P(y_1,\mathrm{\dots },y_n,f(y_1,\mathrm{\dots },y_n)),$$

tomamos elementos $\{c_1,\mathrm{\dots },c_n\}$ arbitrarios del dominio. Por construcción, $f(c_1,\mathrm{\dots },c_n)=b$ para algún $b\in A$ y $(c_1,\mathrm{\dots },c_n,b)\in P^{{ℳ}^{\prime }}$. Como $c_1,\mathrm{\dots },c_n$ eran arbitrarios:

$${ℳ}^{\prime }\vDash \forall y_1\mathrm{\dots }\forall y_{n}P(y_1,\mathrm{\dots },y_n,f(y_1,\mathrm{\dots },y_n))$$

Esto completa una dirección de la prueba del Teorema de Skolem. La prueba de la inversa se deja como ejercicio.

4 Ejemplo

Transformar el siguiente enunciado a forma clausular.

$$\neg \exists y\left(P(y)\wedge \forall z(R(z)\to Q(y,z))\right)$$

1. La fórmula queda igual.

2. $\neg \exists y\left(P(y)\wedge \forall z(\neg R(z)\vee Q(y,z))\right)$.

4. La fórmula queda igual.

5. $\forall y\exists z\left(\neg P(y)\vee (R(z)\wedge \neg Q(y,z))\right)$.

6. $\forall y\exists z\left((\neg P(y)\vee R(z))\wedge (\neg P(y)\vee \neg Q(y,z))\right)$.

7. $\forall y\left((\neg P(y)\vee R(f(y)))\wedge (\neg P(y)\vee \neg Q(y,f(y)))\right)$.

8. $\{\{\neg P(y),R(f(y))\},\{\neg P(y),\neg Q(y,f(y))\}\}$, esta es la forma clausular que buscamos.

Ejercicios 4.1.

Transformar las siguientes fórmulas a su forma clausular.

1. $\forall x\exists y\left(P(x,g(y))\to \neg \forall xQ(x)\right)$.

2. $\forall x\exists y\left(\exists z\forall wR(x,y,z,w)\to \exists vP(v)\right)$.

3. $\forall x\left(P(x)\wedge \neg \exists y(Q(y)\wedge R(x,y))\right)\vee \neg \left(\forall yP(y)\wedge \neg \forall zP(z)\right)$.

4. $\exists x\left(T(x)\wedge \neg Q(x)\right)\to \forall x\left(R(x)\to \neg T(x)\right)$.

5. $\exists x\forall yP(x,y)\to \forall y\exists xP(x,y)$.

6. $\forall x\left(P(x)\to Q(x)\right)\to \left(\forall xP(x)\to \forall xQ(x)\right)$.