Editing Skolem normal form (section)

{{Short description|Formalism of first-order logic}}
In [[mathematical logic]], a [[Well-formed_formula|formula]] of [[first-order logic]] is in '''Skolem normal form''' if it is in [[prenex normal form]] with only [[Universal quantification|universal first-order quantifiers]]. 

Every first-order [[Well-formed formula|formula]] may be converted into Skolem normal form while not changing its [[satisfiability]] via a process called '''Skolemization''' (sometimes spelled '''Skolemnization'''). The resulting formula is not necessarily [[logical equivalence|equivalent]] to the original one, but is [[equisatisfiable]] with it: it is satisfiable if and only if the original one is satisfiable.<ref>{{cite web|title=Normal Forms and Skolemization|url=http://www.mpi-inf.mpg.de/departments/rg1/teaching/autrea-ss10/script/lecture10.pdf|publisher=[[Max-Planck-Institut für Informatik]]|accessdate=15 December 2012}}</ref>

Reduction to Skolem normal form is a method for removing [[existential quantification|existential quantifiers]] from [[formal logic]] statements, often performed as the first step in an [[automated theorem prover]].