Este artigo foi avaliado automaticamente com qualidade 2 Para o WikiProjeto:Lógica importância ainda não avaliada Se não tiver suas questões respondidas nesta página de discussão procure o(s) wikiprojeto(s) acima.
Este artigo foi desenvolvido e/ou revisto no âmbito de uma atividade educacional em dezembro de 2006. Estão disponíveis mais detalhes .
3) Remova os quantificadores universais
No item 5 - mudar a redação para: 5) Coloque na forma de cláusula, substituindo
C
1
∧
.
.
.
∧
C
n
{\displaystyle C_{1}\land ...\land C_{n}}
{
C
1
,
.
.
.
,
C
n
}
{\displaystyle \{C_{1},...,C_{n}\}}
Passo 5) Colocar na forma de cláusulas:
{
¬
P
(
x
)
,
f
(
x
)
∨
P
(
g
(
x
)
,
x
)
}
{\displaystyle \{\lnot P(x),f(x)\lor P(g(x),x)\}}
Remover o passo 6
Exemplo 2 :
∀
x
(
¬
∀
y
(
P
(
x
,
y
)
∧
∀
z
¬
R
(
y
,
z
)
)
∧
∀
y
¬
P
(
x
,
y
)
)
{\displaystyle \forall x(\lnot \forall y(P(x,y)\land \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))}
∀
x
(
¬
∀
y
(
P
(
x
,
y
)
∧
∀
z
¬
R
(
y
,
z
)
)
∧
∀
y
¬
P
(
x
,
y
)
)
{\displaystyle \forall x(\lnot \forall y(P(x,y)\land \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))}
∀
x
(
∃
y
¬
(
P
(
x
,
y
)
∧
∀
z
¬
R
(
y
,
z
)
)
∧
∀
y
¬
P
(
x
,
y
)
)
{\displaystyle \forall x(\exists y\lnot (P(x,y)\land \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))}
∀
x
(
∃
y
(
¬
P
(
x
,
y
)
∨
¬
∀
z
¬
R
(
y
,
z
)
)
∧
∀
y
¬
P
(
x
,
y
)
)
{\displaystyle \forall x(\exists y(\lnot P(x,y)\lor \lnot \forall z\lnot R(y,z))\land \forall y\lnot P(x,y))}
∀
x
(
∃
y
(
¬
P
(
x
,
y
)
∨
∃
z
R
(
y
,
z
)
)
∧
∀
y
¬
P
(
x
,
y
)
)
{\displaystyle \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:
∀
x
∃
y
1
∃
z
∀
y
2
(
(
¬
P
(
x
,
y
1
)
∨
R
(
y
1
,
z
)
)
∧
¬
P
(
x
,
y
2
)
)
{\displaystyle \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
)
]
{\displaystyle [y_{1}:=f(x),z:=g(x)]}
∀
x
∀
y
2
(
(
¬
P
(
x
,
f
(
x
)
)
∨
R
(
f
(
x
)
,
g
(
x
)
)
∧
¬
P
(
x
,
y
2
)
)
{\displaystyle \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
∀
x
{\displaystyle \forall x}
∀
y
2
{\displaystyle \forall y_{2}}
(
(
¬
P
(
x
,
f
(
x
)
)
∨
R
(
f
(
x
)
,
g
(
x
)
)
∧
¬
P
(
x
,
y
2
)
)
{\displaystyle ((\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:
{
¬
P
(
x
,
f
(
x
)
)
∨
R
(
f
(
x
)
,
g
(
x
)
)
,
¬
P
(
x
,
y
2
)
}
{\displaystyle \{\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) Responder
![{\displaystyle [y_{1}:=f(x),z:=g(x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e92ea767e2a0a0966eaa7e80adfd7e9178838ee7)
