Skolem normal form

Summary

A sentence is in Skolem normal form when it is in prenex normal form and has only universal quantifiers. Every first-order sentence can be turned into one in Skolem normal form by replacing each existential quantifier with a new function symbol. The new sentence is not equivalent to the old one, but it is satisfiable exactly when the old one is. This makes Skolem normal form the starting point of Herbrand's theorem and of resolution theorem proving.