Fonction de Skolem

Définition

xxxxxxx

Français

xxxxxxx

Anglais

Skolem functions

Universally quantified variables can be handled (and are handled in Prolog) simply by assuming that any variable is universally quantified. Existentially quantified variables must thus be removed in some way. This is handled by a technique called skolemization.

In its simplest form, skolemization replaces the variable with a new constant, called a Skolem constant. For example, the formula:

exists(y, forall(x, loves(x, y))

would be encoded as an expression such as

loves(X, sk1),

where sk1 is a new constant that stands for the object that is asserted to exist, i.e. the person (or whatever) that is loved by every X.

Quantifier scoping dependencies are shown using new functions called Skolem functions. For example, the formula:

forall(y, exists(x, loves(x,y))

would be encoded as an expression such as

Source : UNWS Natural Language Processing Dictionary