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

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 Resource. https://mathworld.wolfram.com/SkolemizedForm.html

Subject classifications