fonction de Skolem

CONT: La skolémisation d'une formule consiste à supprimer les quantificateurs selon la convention que les variables (...) sont remplacées par des fonctions (dites de skolem) dépendant des variables universellement quantifiées (...) Le choix d'une fonction de skolem judicieuse est un problème dont l'automatisation n'est pas encore envisagée à notre connaissance. (...) Dans les techniques d'extraction de connaissances des experts pour construire un Système Expert, il ne faut pas oublier de faire préciser les bonnes fonctions de skolémisation par l'expert.

CONT: ... for each x, the existence of a y is postulated such that G(y,x). However how to find this y for a given x is generally not explicitly described. The existence of y is a priori quite non-procedural, and the same x may give a different y at different times. However a unique function f may be postulated such that for each x a unique y greater than x is computed. It is not necessary to give this function any interpretation, just a name f(x). Thus the operator and the y variable are no longer needed. ... Such a function is called a Skolem function after Norwegian logician Thoralf Skolem who proved that the validity of the formula was preserved by this simplification.