TOPICS
Search

Skolem Function


Consider a formula in prenex normal form,

 Q_1x_1...Q_nx_nN.

If Q_i is the existential quantifier (1<=i<=n) and x_k, ..., x_m are all the universal quantifier variables such that 1<=k, m<i, then introduce the new function symbol f and term f(x_k,...,x_m). (If i=1, then f is a constant.) This function is called Skolem function (or Herbrand function).

Now replace all occurrences of x_i by this term and remove Q_i. When all existential quantifiers are removed, convert N into conjunctive normal form. This process, which usually termed skolemization, results in a formula in Skolemized form. The resulting formula is unsatisfiable iff the source formula is unsatisfiable. Note that if the source formula is satisfiable, it is not necessarily equivalent to the resulting formula.


See also

Skolemized Form

This entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha

References

Chang, C.-L. and Lee, R. C.-T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.Kleene, S. C. Mathematical Logic. New York: Dover, 2002.

Referenced on Wolfram|Alpha

Skolem Function

Cite this as:

Sakharov, Alex. "Skolem Function." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/SkolemFunction.html

Subject classifications