fonction de Skolem
- Domaine
-
- intelligence artificielle
- Dernière mise à jour
Définition :
Fonction introduite pour éliminer les quantificateurs existentiels.
Termes privilégiés :
- fonction de Skolem n. f.
- fonctions de Skolem n. f. pl.
Traductions
-
anglais
Auteur : Office québécois de la langue française,Note :
When Skolemizing a formula of "predicate calculus", Skolem functions are employed where the "existential quantifier" to be removed lies within the scope of "universal quantifiers". The variable bound by the existential quantifier is replaced by a term composed of an arbitrary function, a Skolem function, which has as arguments the variables of those universal quantifiers, because the value of the variable depends on those quantifiers.
Terme :
- Skolem function