# 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 is a formula with free variables

, , , , then is replaced by

, and is replaced by

, where 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.