Skolem normal form

A formula obtained by eliminating existential quantifiers through Skolem constants or functions, leaving only universal quantifiers. It is equisatisfiable with the original formula, but need not be logically equivalent to it.

Skolemization: A transformation that replaces existentially quantified variables with fresh constants or functions to preserve satisfiability. This is the operation that produces Skolem normal form.
First-order logic: A formal system with variables, predicates, functions, and quantifiers over individual objects. Skolem normal form is defined for formulas in this logic.
Resolution (logic): A rule of inference that derives a clause by eliminating complementary literals. Resolution provers commonly use Skolemized clauses as input.
Logical equivalence: A relation between formulas that have the same truth value under every interpretation. Skolemization generally preserves satisfiability, not this stronger relation.
Prenex normal form: A formula form in which all quantifiers precede a quantifier-free matrix. Moving quantifiers to the front exposes the dependencies used to choose Skolem functions.
Existential quantification: A quantifier asserting that a predicate holds for at least one object in its domain. Eliminating existential quantifiers is the defining step of Skolem normal form.
Clause normal form: A conjunction of clauses, each clause being a disjunction of literals. Skolemization is typically followed by conversion to clauses for resolution.
Conjunctive normal form: A formula expressed as a conjunction of clauses, each clause a disjunction of literals. Unlike Skolem normal form, this shape specifies Boolean structure rather than quantifier elimination.
Skolem function: A fresh function symbol that represents a witness for an existential variable as a function of preceding universal variables. Its arguments encode which universal variables an existential witness may depend on.
Quantifier scope: The portion of a formula governed by a particular quantifier. Scope determines which variables are bound and how quantifier dependencies are read.

Linked from 2 pages

Herbrand's theoremRelated: Normal-form methods make the theorem's ground-instance formulation precise.