Skolemização: diferenças entre revisões

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 o quantificador principal é o existencial, a fórmula obtida removendo esse quantificador através da skolemização pode ser gerada. Por exemplo, se <math>\exists x . \Phi(x,y_1,\ldots,y_n)</math> ocorrer em tableaux, onde <math>x,y_1,\ldots,y_n</math> sejam variáveis livres de <math>\Phi(x,y_1,\ldots,y_n)</math>, quando <math>\Phi(f(y_1,\ldots,y_n),y_1,\ldots,y_n)</math> puder ser adicionado à mesma ramificação de tableaux. Esta adição não altera a sua satisfatibilidade: todo modelo da fórmula antiga pode ser expandido, adicionando um valor apropiadoapropriado à <math>f</math> em um modelo da nova fórmula.

Esta forma de skolemização é atualmente um progresso da skolemização "clássica", que todas as variáveis livres na fórmula, são substituidas por um '''termo de Skolem'''. Esta é uma melhoria porque a semântica de tableaux pode implicitamente colocar a fórmula no escopo de algumas variáveis quantificadas universalmente, que não estao 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 possa ser usada, é aplicar o mesmo símbolo de uma '''função de Skolem''' para as fórmulas que são identicasidênticas.