Convertir un WFF en una forma clausal

Question

Se me plantea la siguiente pregunta:

Convierta el siguiente WFF en forma clausal: \begin{equation*} \forall(X)(q(X)\to(\exists(Y)(\neg(p(X,Y)\vee r(X,Y))\to h(X,Y))\wedge f(X))) \end{equation*}

Esto es lo que he conseguido hasta ahora, pero no estoy seguro de que esté en la forma adecuada al final.

En primer lugar, eliminar las implicaciones: \begin{gather} \forall(X)(q(X)\to(\exists(Y)((p(X,Y)\vee r(X,Y))\vee h(X,Y))\wedge f(X)))\\ \forall(X)(\neg q(X)\vee(\exists(Y)((p(X,Y)\vee r(X,Y))\vee h(X,Y))\wedge f(X))) \end{gather} Mueve los cuantificadores al frente: \begin{gather} \forall(X)\exists(Y)(\neg q(X)\vee((p(X,Y)\vee r(X,Y)\vee h(X,Y))\wedge f(X))) \end{gather} Skolemizar cuantificadores existenciales con $g(X)/Y$ : \begin{gather} \forall(X)(\neg q(X)\vee((p(X,g(X))\vee r(X,g(X))\vee h(X,g(X)))\wedge f(X))) \end{gather} Eliminar los cuantificadores universales: \begin{gather} \neg q(X)\vee((p(X,g(X))\vee r(X,g(X))\vee h(X,g(X)))\wedge f(X)) \end{gather}

Answer 1

Para escribir $\neg q(X)\lor\Big(\big(p(X,g(X))\lor r(X,g(X))\lor h(X,g(X))\big)\land f(X)\Big)$ en forma clausal, primero hay que ponerlo en forma normal conjuntiva. Para ello, puedes distribuir la primera disyunción sobre la paréntesis para obtener: $$\big(\neg q(X)\lor f(X)\big)\land\big(\neg q(X)\lor p(X,g(X))\lor r(X,g(X))\lor h(X,g(X))\big)$$ Cada parte de la conjunción corresponde a una cláusula, que es una disyunción finita de átomos. Así, la forma clausal de tu wff original es: $$\bigg\{\Big\{\neg q(X),f(X)\Big\},\Big\{\neg q(X),p(X,g(X)),r(X,g(X)),h(X,g(X))\Big\}\bigg\}$$