Catalogue of Artificial Intelligence Techniques
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.
- Chang, C.L. and Lee, R.C., Symbolic Logic and Mechanical Theorem Proving
, Academic Press, New York, 1973.