Skolemized Form

A formula of first-order logic is said to be in Skolemized form (sometimes also called Skolem standard form or universal form) if it is of the form

  forall x_1... forall x_nM,

where M is a quantifier-free formula in conjunctive normal form known as the matrix of the formula in question. Since M is a conjunction of clauses each of which is a disjunction of literals, M is often viewed as a set of the clauses. The process of placing a formula in Skolemized form is known as Skolemization.

See also

Skolem Function

Portions of this entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha

Cite this as:

Sakharov, Alex and Weisstein, Eric W. "Skolemized Form." From MathWorld--A Wolfram Web Resource.

Subject classifications