Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML


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.



Add Comment

No comments.