Skolem Normal Form (Mathematical Logic)

In mathematical logic, reducing to skolem normal form is a method for removing existential quantifiers from formal logic statements – often performed as the first step in an automated theorem prover.

A formula of first-order logic is in skolem normal form if it is in prenex normal form with only universal first-order quantifiers. The resulting skolem form is not necessarily equivalent to the original one. It only preserves satisfiability, i.e. it is satisfiable if and only if the original one is satisfiable.

References

• https://en.wikipedia.org/wiki/Skolem_normal_form