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]] 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 equivalente à original, mas é [http://pt.wikipedia.org/wiki/Valoração [Satisfazibilidade|satisfatível]] [[Se e somente se|se e somente se]] a original também o for.