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 meem tableautableaux, 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 apropiado à <math>f</math>, a um modelo da nova fórmula.