•Eliminação dos quantificadores existenciais (Skolemização ou Funções de Skolem)
–Quando
uma fórmula está na forma normal Prenex, pode-se eliminar os quantificadores existenciais por uma função, se as variáveis estiverem no escopo do quantificador universal; caso estejam fora,
substitui-se por uma
constante.
–As
constantes e funções usadas para substituir as variáveis existenciais são
chamadas constante e
funções de Skolem
•Ex.: "x $ y P(x,y)
• Skolemizando: "x P(x,f(x))
•onde f(x) tem por único propósito
garantir que existe algum
valor (y) que depende de x
pois está dentro do seu escopo. No entanto, se o quantificador existencial não residir no escopo do quantificador universal, como em $
y "x P(x,y), a variável quantificada existencialmente será
substituída por uma constante "x P(x,a) que assegure sua existência,
assim como sua
independência de qualquer outra variável.
–Por
fim, abandona-se os quantificadores pré-fixados, e obtém-se uma sentença na forma CLAUSAL.
–CLÁUSULA:
É uma disjunção de literais
•