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

Uma fórmula da [[Lógica de primeira ordem|lógica de primeira ordem]] está na '''forma normal de Skolem''' (nome devido à [[Thoralf Skolem|Thoralf Skolem]]), se sua [[Forma normal prenex|forma normal prenex]] contiver somente quantificadores universais. Cada fórmula de primeira ordem pode ser convertida na forma normal de Skolem através do processo de skolemização. A fórmula resultante deste processo não é necessariamente [[Equivalência lógica|equivalente]] à original, mas é [[Satisfazibilidade|satisfatível]] [[Se e somente se|se e somente se]] a original também o for.