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 A(y) is a formula with free variablesy

, x1 , , xn , then yA(y) is replaced byA(y)

, and yA(y) is replaced byA(f(x1,...,xn))

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



Add Comment

No comments.