Discussão:Forma normal clausal

Coisas para alterar

• No item 3:

3) Remova os quantificadores universais

• No item 5 - mudar a redação para:

5) Coloque na forma de cláusula, substituindo $C_{1}\land ...\land C_{n}$ por $\{C_{1},...,C_{n}\}$.

• No exemplo 1:

Passo 5) Colocar na forma de cláusulas:

$\{\lnot P(x),f(x)\lor P(g(x),x)\}$

Remover o passo 6

• Mudar o exemplo 2:

Exemplo 2: $\forall x(\lnot \forall y(P(x,y)\land \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))$ Passo 1) Colocar a fórmula na forma normal da negação:

$\forall x(\lnot \forall y(P(x,y)\land \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))$

$\forall x(\exists y\lnot (P(x,y)\land \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))$

$\forall x(\exists y(\lnot P(x,y)\lor \lnot \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))$

$\forall x(\exists y(\lnot P(x,y)\lor \exists zR(y,z))\land \forall y\lnot P(x,y))$

Passo 2) Skolemizar a fórmula:

$\forall x\exists y_{1}\exists z\forall y_{2}((\lnot P(x,y_{1})\lor R(y_{1},z))\land \lnot P(x,y_{2}))$

Substituindo $[y_{1}:=f(x),z:=g(x)]$

$\forall x\forall y_{2}((\lnot P(x,f(x))\lor R(f(x),g(x))\land \lnot P(x,y_{2}))$

Passo 3) Remover os quantificadores universais $\forall x$ e $\forall y_{2}$:

$((\lnot P(x,f(x))\lor R(f(x),g(x))\land \lnot P(x,y_{2}))$

Passo 4) A fórmula já está na forma normal conjuntiva.

Passo 5) Colocar na fórma de cláusulas:

$\{\lnot P(x,f(x))\lor R(f(x),g(x)),\lnot P(x,y_{2})\}$

—comentário não assinado de Arthorius (discussão • contrib) 12h27min de 20 de dezembro de 2006 (UTC)