Skolemização

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

Uma fórmula da lógica de primeira ordem está na forma normal de Skolem (nome devido à Thoralf Skolem), se sua forma normal prenex contiver somente quantificadores universais. Cada fórmula de primeira ordem pode ser convertida na forma normal de Skolem por meio do processo de skolemização. A fórmula resultante deste processo não é necessariamente equivalente à original, mas é satisfatível se e somente se a original também o for.


A skolemização é feita substituindo cada variável \qquad y, quantificada existencialmente, por um termo f(x_1,\ldots,x_n) no qual o símbolo de função \qquad f é uma nova função (nao existe outra ocorrência dele na fórmula). Se a fórmula estiver na forma normal prenex, x_1,\ldots,x_n são as variáveis universalmente quantificadas cujos quantificadores precedem a variável \qquad y. Podemos dizer que \exists y cai sob o escopo dos quantificadores universais que o precedem. A função \qquad f introduzida nesse processo é dita função de Skolem e o termo é dito termo de Skolem.


No caso da ocorrência de uma variável \qquad y quantificada existencialmente ( \exists y ), onde essa quantificação não é precedida por um quantificador universal \forall x, então a variável \qquad y é substituída por uma constante.


Como funciona[editar | editar código-fonte]

A skolemização trabalha aplicando a relação de equivalência da lógica de segunda ordem juntamente com a definição de satisfatibilidade da primeira ordem. A equivalência é feita "movendo" o quantificador existencial para antes do quantificador universal.


\forall x \exists y . R(x,y) \iff \exists f \forall x . R(x,f(x))\mbox{.}

Intuitivamente, a sentença "Para todo x existe um y tal que R(x,y)" é convertida para a forma equivalente "Existe uma função f em x, introduzida por y, para todo x preso no escopo de R(x,f(x))".

Esta equivalência é útil pois a definição de satisfatibilidade da lógica de primeira ordem é implícita nos quantificadores existenciais sobre um símbolo de função. Em resumo, uma fórmula de primeira ordem \qquad \Phi é satisfatível se existir um modelo \qquad M tal que, para todo valor aplicado à variável livre \qquad \mu da fórmula, a fórmula seja verdadeira. Desde que o modelo contenha o valor de todos os símbolos de função, toda função de Skolem é implicitamente existencialmente quantificada. No exemplo acima, \forall x . R(x,f(x)) é satisfativel se e somente se existir um modelo \qquad M, que contenha um valor para \qquad f, tal que \forall x . R(x,f(x)) é verdade para todos os possíveis valores de suas variáveis livres (neste caso nenhuma). Esta mesma fórmula pode ser expressa em segunda ordem como \exists f \forall x . R(x,f(x)), que é satisfativelmente equivalente à \forall x \exists y . R(x,y).

No meta-resultado, a satisfatibilidade de primeira ordem pode ser escrita como \exists M \forall \mu ~.~ ( M,\mu \models \Phi ), onde \qquad M é um modelo e \qquad \mu é o valor da variável. Desde que os modelos de primeira ordem contenham o valor de todo símbolo de função, toda função de Skolem \qquad \Phi contém implicitamente um quantificador existencial \exists M. Em conseqüência, após ter substituído o quantificador existencial sobre variáveis que estão quantificadas existencialmente em funções na parte frontal da fórmula, a fórmula ainda pode ser tratada como sendo de primeira ordem removendo estes quantificadores existenciais. Esta etapa final do tratamento \exists f \forall x . R(x,f(x)) como \forall x . R(x,f(x)) pode ser realizada porque as funções estão implicitamente existencialmente quantificadas em \exists M de acordo com definição de satisfatibilidade da lógica de primeira ordem.

A exatidão do processo de skolemização é mostrada na fórmula F_1 = \forall x_1 \dots \forall x_n \exists y R(x_1,\dots,x_n,y). Esta fórmula é satisfeita por um modelo \qquad M se e somente se para todo possível valor de x_1,\dots,x_n, no modelo, existe um valor para \qquad y que torne R(x_1,\dots,x_n,y) verdadeiro. Pelo axioma da escolha, existe uma função \qquad f tal que y = f(x_1,\dots,x_n). Em consequência, a fórmula F_2 = \forall x_1 \dots \forall x_n R(x_1,\dots,x_n,f(x_1,\dots,x_n)) é satisfatível, pois a mesma obteve um modelo ao se adicionar o valor de \qquad f a \qquad M. Isto mostra que F_1 é satisfatível somente se F_2 também for. De outra maneira, se F_2 for satisfatível, então existe um modelo \qquad M que lhe satisfaça; este modelo aplica um valor à função \qquad f tal que, para todo valor de x_1,\dots,x_n, a fórmula R(x_1,\dots,x_n,f(x_1,\dots,x_n)) fica presa. Em conseqüência, F_1 é satisfeito pelo mesmo modelo pois pode fazer uma escolha para todo valor de x_1,\ldots,x_n, o valor y=f(x_1,\dots,x_n), onde o valor de \qquad f é obtido de acordo com \qquad M.

Usos da skolemização[editar | editar código-fonte]

Um dos usos da skolemização é a prova automatizada de teoremas. Por exemplo, no método analítico de tableaux, sempre que uma fórmula cujo quantificador principal é o existencial, a fórmula obtida removendo esse quantificador por meio da skolemização pode ser gerada. Por exemplo, se \exists x . \Phi(x,y_1,\ldots,y_n) ocorrer em um tableau, onde x,y_1,\ldots,y_n sejam variáveis livres de \Phi(x,y_1,\ldots,y_n), quando \Phi(f(y_1,\ldots,y_n),y_1,\ldots,y_n) puder ser adicionado à mesma ramificação do tableau. Esta adição não altera a sua satisfatibilidade: todo modelo da fórmula antiga pode ser expandido, adicionando um valor apropriado à f em um modelo da nova fórmula.

Esta forma de skolemização é atualmente um progresso da skolemização "clássica", na qual todas as variáveis livres na fórmula são substituidas por um termo de Skolem. Esta é uma melhoria porque a semântica de tableau pode implicitamente colocar a fórmula no escopo de algumas variáveis quantificadas universalmente, que não estão em sua fórmula; estas variáveis não fazem parte de um termo de Skolem, quando deveriam fazer, de acordo com a definição original de skolemização. Uma outra melhoria que pode ser usada é aplicar o mesmo símbolo de uma função de Skolem para as fórmulas que são idênticas.

Exemplos[editar | editar código-fonte]

  • 1. Considere a fórmula \qquad \alpha, que está na forma normal prenex:
\exists y .\forall x_1 .\forall x_2 .\exists z .R(y,x_1 , x_2 , z)

Eliminando os quantificadores existenciais em \qquad \alpha por meio do processo de skolemização, obtemos a seguinte formula em sua forma normal Skolem:

\forall x_1 .\forall x_2 R(a,x_1 ,x_2 ,f(x_1 ,x_2))

Note que no processo de skolemização a variável \qquad y foi substituída pela constante \qquad a, pois o quantificador existencial \exists y não é precedido por nenhum quantificador universal. Já a variável \qquad z foi substituída por um termo de função \qquad f(x_1 ,x_2), já que o quantificador existencial \exists z é precedido por duas quantificações universais, \forall x_1 e \forall x_2.

  • 2. Considere a fórmula \qquad \beta, que está na forma normal prenex:
\forall x_2 .\forall x_4 .\exists x_1 .\forall x_3 .\exists x_5 .\lnot (P(x_1,x_2) \rightarrow \lnot  (P(x_3,x_4) \land R(x_5)))

Eliminando os quantificadores existenciais em \qquad \beta por meio do processo de skolemização, obtemos a seguinte fórmula em sua forma normal de Skolem:

\forall x_2 .\forall x_4 .\forall x_3 .\lnot (P(f(x_2, x_4),x_2) \rightarrow \lnot (P(x_3,x_4) \land R(g(x_2, x_4, x_3))))

Note que:

No processo de skolemização, a variável \qquad x_1 foi substituída pelo termo de função \qquad f(x_2, x_4) e a variável \qquad x_5 foi substituída pelo termo de outra função \qquad g(x_2, x_4, x_3).

Fazemos isso porque, na forma normal prenex:

Os quantificadores universais \forall x_2 e \forall x_4 precedem o quantificador existencial \exists x_1;

Os quantificadores universais \forall x_2 e \forall x_4 e \forall x_3 precedem o quantificador existencial \exists x_5.

Ver também[editar | editar código-fonte]

Ligações externas[editar | editar código-fonte]