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 , quantificada existencialmente, por um termo no qual o símbolo de função é uma nova função (nao existe outra ocorrência dele na fórmula). Se a fórmula estiver na forma normal prenex, são as variáveis universalmente quantificadas cujos quantificadores precedem a variável . Podemos dizer que cai sob o escopo dos quantificadores universais que o precedem. A função introduzida nesse processo é dita função de Skolem e o termo é dito termo de Skolem.


No caso da ocorrência de uma variável quantificada existencialmente , onde essa quantificação não é precedida por um quantificador universal , então a variável é 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.


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 é satisfatível se existir um modelo tal que, para todo valor aplicado à variável livre 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, é satisfativel se e somente se existir um modelo , que contenha um valor para , tal que é 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 , que é satisfativelmente equivalente à .

No meta-resultado, a satisfatibilidade de primeira ordem pode ser escrita como , onde é um modelo e é 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 contém implicitamente um quantificador existencial . 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 como pode ser realizada porque as funções estão implicitamente existencialmente quantificadas em 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 . Esta fórmula é satisfeita por um modelo se e somente se para todo possível valor de , no modelo, existe um valor para que torne verdadeiro. Pelo axioma da escolha, existe uma função tal que . Em consequência, a fórmula é satisfatível, pois a mesma obteve um modelo ao se adicionar o valor de a . Isto mostra que é satisfatível somente se também for. De outra maneira, se for satisfatível, então existe um modelo que lhe satisfaça; este modelo aplica um valor à função tal que, para todo valor de , a fórmula fica presa. Em conseqüência, é satisfeito pelo mesmo modelo pois pode fazer uma escolha para todo valor de , o valor , onde o valor de é obtido de acordo com .

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 ocorrer em um tableau, onde sejam variáveis livres de , quando 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 à 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 , que está na forma normal prenex:

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

Note que no processo de skolemização a variável foi substituída pela constante , pois o quantificador existencial não é precedido por nenhum quantificador universal. Já a variável foi substituída por um termo de função , já que o quantificador existencial é precedido por duas quantificações universais, e .

  • 2. Considere a fórmula , que está na forma normal prenex:

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

Note que:

No processo de skolemização, a variável foi substituída pelo termo de função e a variável foi substituída pelo termo de outra função .

Fazemos isso porque, na forma normal prenex:

Os quantificadores universais e precedem o quantificador existencial ;

Os quantificadores universais e e precedem o quantificador existencial .

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

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