# Catalogue of Artificial Intelligence Techniques

## Skolemisation

**Keywords:**
Prenex normal form, Skolem function, mathematical
logic, quantifiers

### Categories: Knowledge Representation , Logic Programming , Theorem Proving

Author(s): **Alan Bundy**

A technique borrowed from mathematical logic (and named after the mathematician Skolem), but much used in Automatic Theorem Proving, for removing quantifiers from Predicate Calculus formulae. If $A(y)$ is a formula with free variables$y$

, ${x}_{1}^{}$ , $\dots $ , ${x}_{n}^{}$ , then $\forall yA(y)$ is replaced by$A(y)$

, and $\exists yA(y)$ is replaced by$A(f({x}_{1}^{},\mathrm{...},{x}_{n}^{}))$

, where $f$ is a new Skolem function. The technique is usually applied to formulae which have all their quantifiers at the front (prenex normal form), but can be adapted to any formula. It produces a formula which has a model if and only if the original formula does. It is one of the techniques used in turning a formulae into Clausal Form.

### References:

- Chang, C.L. and Lee, R.C.,
*Symbolic Logic and Mechanical Theorem Proving*, Academic Press, New York, 1973.

### Comments:

No comments.