TERMIUM Plus^®

Record 1,  Textual support,  English

Record number: 1, Textual support number: 1 DEF

A function introduced by Thoralf Skolem as a technique for eliminating quantifiers.  2, record 1, English, - Skolem%20function

Record number: 1, Textual support number: 1 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.  3, record 1, English, - Skolem%20function

Record 1,  Textual support,  French

Record number: 1, Textual support number: 1 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.  2, record 1, French, - fonction%20de%20Skolem

Record 1,  Textual support,  Spanish