Conversión de fórmulas de lógica de predicados a la forma normal de Skolem

Question

Me gustaría transformar las siguientes fórmulas de lógica de predicados en Forma normal Skolem , simplificar en la medida de lo posible. Intento mostrar mi trabajo con claridad, escribiendo cada paso en una línea propia e indicando cómo se ha obtenido. Sin embargo, no estoy seguro de si lo estoy haciendo correctamente (simplificando en los lugares adecuados, eliminando suficientes paréntesis, etc.) y con eficacia.

Estoy intentando utilizar lo siguiente algoritmo de skolemización :

1. Sustituya todas las apariciones de , , .
2. Mueve la negación hacia dentro.
3. Normalizar las variables aparte.
4. Reescribir cuantificadores existenciales utilizando Funciones Skolem.
5. Mover cuantificadores universales al frente.
6. Utiliza la Ley de Distributividad.

a) $x (dog(x) y (dog(y) admires(y, x)))$

$$x \space (dog(x) \negy \space (dog(y)\wedge admires(y, x))) \qquad \text{(def. )}$$ $$x \space (dog(x) y\space \neg(dog(y)\wedge admires(y, x))) \qquad \text{(De Morgan)}$$ $$x \space (dog(x) y\space (\neg dog(y)\vee \neg admires(y, x))) \qquad \text{(De Morgan)}$$ $$x_1 \space (dog(x_1) y_1\space (\neg dog(y_1)\vee \neg admires(y_1, x_1))) \qquad \text{(Standardize)}$$ $$((dog(dog\_x) (\neg dog(dog\_y)\vee \neg admires(dog\_y, dog\_x))) \qquad \text{(Skolemize)}$$ $$((dog(dog\_x) (\neg dog(dog\_y))) \vee (dog(dog\_x) \neg admires(dog\_y, dog\_x))) \qquad \text{(Distributivity)}$$ ... ¿alguna conversión de forma normal Disyuntiva a Conjuntiva? (no sé cómo)

b) $x (y (dog(y) admires(y, x)) y (dog(y) stronger(x, y)))$

$$x (y (\neg dog(y) \vee admires(y, x)) y (\neg dog(y) \vee stronger(x, y))) \qquad \text{(def. )}$$ $$x (y (\neg dog(y) \vee admires(y, x)) y (\neg dog(y) \vee stronger(x, y)) )\space \space (y (\neg dog(y) \vee stronger(x, y)) y (\neg dog(y) \vee admires(y, x))) \qquad \text{(def. )}$$ $$x (\neg y (\neg dog(y) \vee admires(y, x)) \vee y (\neg dog(y) \vee stronger(x, y)) )\space \space (\neg y (\neg dog(y) \vee stronger(x, y)) \vee (y (\neg dog(y) \vee admires(y, x))) \qquad \text{(def. )}$$ $$x (x \neg(\neg dog(y) \vee admires(y, x)) \vee y (\neg dog(y) \vee stronger(x, y)) )\space \space (x \neg(\neg dog(y) \vee stronger(x, y)) \vee (y (\neg dog(y) \vee admires(y, x))) \qquad \text{(De Morgan)}$$ $$x (x (\neg\neg dog(y) \neg admires(y, x)) \vee y (\neg dog(y) \vee stronger(x, y)) )\space \space (x (\neg\neg dog(y) \neg stronger(x, y)) \vee (y (\neg dog(y) \vee admires(y, x))) \qquad \text{(De Morgan)}$$ $$x (x (dog(y) \neg admires(y, x)) \vee y (\neg dog(y) \vee stronger(x, y)) )\space \space (x (dog(y) \neg stronger(x, y)) \vee (y (\neg dog(y) \vee admires(y, x))) \qquad \text{(Double Negation)}$$ $$x (x_1 (dog(y) \neg admires(y, x_1)) \vee y (\neg dog(y) \vee stronger(x_1, y)) )\space \space (x_2 (dog(y) \neg stronger(x_2, y)) \vee (y (\neg dog(y) \vee admires(y, x_2))) \qquad \text{(Standardize)}$$ $$x ((dog(y) \neg admires(y, dog\_x)) \vee y (\neg dog(y) \vee stronger(dog\_x, y)) )\space \space ((dog(y) \neg stronger(dog\_z, y)) \vee (y (\neg dog(y) \vee admires(y, dog\_z))) \qquad \text{(Skolemize)}$$ ... algún paso distributivo para traer cuantificadores universales al frente y hacer matriz conjuntiva forma normal? (no estoy seguro de cómo)

---

Segundo intento tras revisar las respuestas: a)

$$x \space (dog(x) y (dog(y) admires(y, x)))$$

$$x \space (dog(x) y \space (\neg dog(y) admires(y, x))) \qquad \text{(def. )}$$

$$x y \space (dog(x) \space (\neg dog(y) admires(y, x))) \qquad \text{(by Prenex Law)}$$

$$x_1 y \space (dog(x_1) \space (\neg dog(y) admires(y, x_1))) \qquad \text{(Standardize)}$$

$$y \space (dog(dog_x) \space (\neg dog(y) admires(y, dog_x))) \qquad \text{(Skolemize) Done!}$$

b)

$$x (y (dog(y) admires(y, x)) y (dog(y) stronger(x, y)))$$

$$x (y (\neg dog(y) admires(y, x)) y (\neg dog(y) stronger(x, y))) \qquad \text{(def. )}$$

$$x ((y (\neg dog(y) \vee admires(y, x)) y (\neg dog(y) \vee stronger(x, y)) )\space \space (y (\neg dog(y) \vee stronger(x, y)) y (\neg dog(y) \vee admires(y, x)))) \qquad \text{(def. )}$$

$$x ((\neg y (\neg dog(y) \vee admires(y, x)) \vee y (\neg dog(y) \vee stronger(x, y)) )\space \space (\neg y (\neg dog(y) \vee stronger(x, y)) \vee y (\neg dog(y) \vee admires(y, x)))) \qquad \text{(def. )}$$

$$x ((y \neg(\neg dog(y) \vee admires(y, x)) \vee y (\neg dog(y) \vee stronger(x, y)) )\space \space (y \neg(\neg dog(y) \vee stronger(x, y)) \vee y (\neg dog(y) \vee admires(y, x)))) \qquad \text{(De Morgan)}$$

$$x ((y (\neg\neg dog(y) \neg admires(y, x)) \vee y (\neg dog(y) \vee stronger(x, y)) )\space \space (y (\neg\neg dog(y) \neg stronger(x, y)) \vee y (\neg dog(y) \vee admires(y, x)))) \qquad \text{(De Morgan)}$$

$$x ((y (dog(y) \neg admires(y, x)) \vee y (\neg dog(y) \vee stronger(x, y)) )\space \space (y (dog(y) \neg stronger(x, y)) \vee y (\neg dog(y) \vee admires(y, x)))) \qquad \text{(Double Negation)}$$

$$x y (y(dog(y) \neg admires(y, x)) \vee (\neg dog(y) \vee stronger(x, y)) )\space \space (y (dog(y) \neg stronger(x, y)) \vee (\neg dog(y) \vee admires(y, x)) \qquad \text{(Scope Change)}$$

$$x y (y_1(dog(y_1) \neg admires(y_1, x)) \vee (\neg dog(y) \vee stronger(x, y)) )\space \space (y_2 (dog(y_2) \neg stronger(x, y_2)) \vee (\neg dog(y) \vee admires(y, x)) \qquad \text{(Standardize)}$$

$$x y ((dog(dog\_y1) \neg admires(dog\_y1, x)) \vee (\neg dog(y) \vee stronger(x, y)) )\space \space ((dog(dog\_y2) \neg stronger(x, dog\_y2)) \vee (\neg dog(y) \vee admires(y, x)) \qquad \text{(Skolemize)}$$

(¿distribuir?)

Answer 1

Para $(a)$ puedes utilizar tablas de verdad. Calcula la tabla de verdad completa de tu fórmula: \begin{array} pp & q & r & s & (p\wedge\neg q)\vee(r\wedge \neg s) & CNF\\ 0 & 0 & 0 & 0 & \underline0 & \_\_\_\_\_ \\ 0 & 0 & 0 & 1 & \underline0 & \_\_\_\_\_ \\ 0 & 0 & 1 & 0 & \underline1 & \_\_\_\_\_ \\ 0 & 0 & 1 & 1 & \underline0 & \_\_\_\_\_ \\ 0 & 1 & 0 & 0 & \underline0 & \_\_\_\_\_ \\ 0 & 1 & 0 & 1 & \underline0 & \_\_\_\_\_ \\ 0 & 1 & 1 & 0 & \underline1 & \_\_\_\_\_ \\ 0 & 1 & 1 & 1 & \underline0 & \_\_\_\_\_ \\ 1 & 0 & 0 & 0 & \underline1 & \_\_\_\_\_ \\ 1 & 0 & 0 & 1 & \underline1 & \_\_\_\_\_ \\ 1 & 0 & 1 & 0 & \underline1 & \_\_\_\_\_ \\ 1 & 0 & 1 & 1 & \underline1 & \_\_\_\_\_ \\ 1 & 1 & 0 & 0 & \underline0 & \_\_\_\_\_ \\ 1 & 1 & 0 & 1 & \underline0 & \_\_\_\_\_ \\ 1 & 1 & 1 & 0 & \underline1 & \_\_\_\_\_ \\ 1 & 1 & 1 & 1 & \underline0 & \_\_\_\_\_ \\ \end{array} Ahora, conociendo los valores, puedes construir tu función en CNF.

Para $(b)$ ha cometido un error en el cuarto paso (de Def $\rightarrow$ a De Morgan) cambiaste la variable $y$ para un $x$ . Si corriges eso creo que puedes, directamente, poner los cuantificadores universales al frente y usar el mismo principio para llevarlo a $CNF$ .

Answer 2

A)

cometes un error en el primer paso:

$\exists x (dog(x) \land \forall y (dog(y) \rightarrow admires(y,x))) \Leftrightarrow $ (por def. $\rightarrow$ )

$\exists x (dog(x) \land \forall y (\neg dog(y) \lor admires(y,x)))$

Observo que en tu algoritmo skolemizas los existenciales antes de sacar (al frente) los cuantificadores Pero en el proceso de sacarlos los cuantificadores pueden cambiar (ver Prenex 7 y 8 belo). Entonces: primero sacar el cuantificador y luego skolemizar. Consejo: intenta sacar primero los existenciales.

Además, cuando al final tienes algo de la forma $P \land (Q \lor R)$ ya está en CNF ... Entonces no distribuir en ese momento.

Por último, he aquí algunas reglas básicas para sacar un cuantificador fuera de los operadores lógicos, donde P no contiene ninguna variable libre x:

Anexo 1: $P \lor \forall x \: \phi(x) \Leftrightarrow \forall x (P \lor \phi(x))$

Anexo 2: $P \lor \exists x \: \phi(x) \Leftrightarrow \exists x (P \lor \phi(x))$

Anexo 3: $P \land \forall x \: \phi(x) \Leftrightarrow \forall x (P \land \phi(x))$

Anexo 4: $P \land \exists x \: \phi(x) \Leftrightarrow \exists x (P \land \phi(x))$

Anexo 5: $P \rightarrow \forall x \: \phi(x) \Leftrightarrow \forall x (P \rightarrow \phi(x))$

Anexo 6: $P \rightarrow \exists x \: \phi(x) \Leftrightarrow \exists x (P \rightarrow \phi(x))$

Anexo 7: $\forall x \: \phi(x) \rightarrow P \Leftrightarrow \exists x (\phi(x) \rightarrow P)$

Anexo 8: $\exists x \: \phi(x) \rightarrow P \Leftrightarrow \forall x (\phi(x) \rightarrow P)$

Así que ten cuidado con esos dos últimos: el cuantificador cambia si lo sacas fuera de un condicional, ¡y es el antecedente de ese condicional!

Y debido a esto último, no existe una equivalencia simple que implique sacar un cuantificador fuera de un bicondicional.

OK, entonces para b)

Eres bueno hasta este punto:

$$∀x ((∃y (dog(y) ∧ \neg admires(y, x)) \vee ∀y (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (∃y (dog(y) ∧ \neg stronger(x, y)) \vee ∀y (\neg dog(y) \vee admires(y, x))))$$

Ahora quieres sacar tus cuantificadores, pero primero debes renombrar las variables, de lo contrario los cuantificadores 'capturarán' variables que no estaban cuantificando. Entonces:

$$∀x ((∃y_1 (dog(y_1) ∧ \neg admires(y_1, x)) \vee ∀y_2 (\neg dog(y_2) \vee stronger(x, y_2)) )\space ∧ \space (∃y_3 (dog(_3) ∧ \neg stronger(x, y_3)) \vee ∀y_4 (\neg dog(y_4) \vee admires(y_4, x))))$$

Vale, ya que lo has reducido todo a las conectivas booleanas $\land$ , $\lor$ y $\not$ y ha trabajado cualquier $\not$ dentro de los cuantificadores, podemos sacar los cuantificadores tal cual. De nuevo, recomiendo sacar primero los existenciales. Así que..:

$$∀x ∃y_1 ∃y_3 ∀y_2 ∀y_4 (( (dog(y_1) ∧ \neg admires(y_1, x)) \vee (\neg dog(y_2) \vee stronger(x, y_2)) )\space ∧ \space ( (dog(_3) ∧ \neg stronger(x, y_3)) \vee (\neg dog(y_4) \vee admires(y_4, x))))$$

Y sí, para su paso final, distribuya cualquier $\lor$ de más de $\land$ 's:

$$∀x ∃y_1 ∃y_3 ∀y_2 ∀y_4 (( (dog(y_1) \lor (\neg dog(y_2) \vee stronger(x, y_2))) ∧ (\neg admires(y_1, x) \vee (\neg dog(y_2) \vee stronger(x, y_2))) )\space ∧ \space ( (dog(_3) \vee (\neg dog(y_4) \vee admires(y_4, x))) ∧ (\neg stronger(x, y_3) \vee (\neg dog(y_4) \vee admires(y_4, x))))$$

Y podemos eliminar algunos paréntesis por asociación:

$$∀x ∃y_1 ∃y_3 ∀y_2 ∀y_4 ( (dog(y_1) \lor \neg dog(y_2) \vee stronger(x, y_2) ∧ (\neg admires(y_1, x) \vee \neg dog(y_2) \vee stronger(x, y_2) ) \space ∧ \space (dog(_3) \vee \neg dog(y_4) \vee admires(y_4, x)) ∧ (\neg stronger(x, y_3) \vee \neg dog(y_4) \vee admires(y_4, x))$$