skolémisation
- Domaines
-
- philosophiethéorie de la connaissance
- intelligence artificielle
- Dernière mise à jour
Définition :
Procédure de logique qui, appliquée à une formule, consiste à en supprimer les quantificateurs existentiels pour les remplacer par des fonctions de skolem. La procédure est appliquée quand la formule d'origine a déjà été transformée en forme normale prénexe.
Notes :
((Procédure définie)) par Thoralf Albert Skolem, mathématicien et logicien norvégien, 1887‑1963. Remplacement d'une variable quantifiée existentiellement par une fonction des variables préalablement quantifiées universellement. Cette fonction est appelée « fonction de Skolem ». S'il n'y a pas de variable quantifiée universellement, la fonction de Skolem est alors une constante. EXEMPLE 1 non formel : la phrase « dans un groupe G, il existe un élément neutre pour la loi de composition interne » devient après skolémisation : « eG est l'élément neutre du groupe G », obtenue en nommant l'élément neutre et en indiquant son rattachement à G. EXEMPLE 2 non formel : considérons la phrase « tous les professeurs sont bien payés ». Sa négation est : « il existe un professeur mal payé », qui devient après skolémisation « JE suis mal payé ».
La réduction d'une formule à la forme de Skolem requiert deux opérations préalables : mettre la formule sous forme prénexe composée d'un préfixe et d'une matrice, et transformer la matrice en forme conjonctive normale. Le résultat est une forme prénexe close.
Terme privilégié :
- skolémisation n. f.
Traductions
-
anglais
Auteur : Office québécois de la langue française,Note :
It occurs after the formula has been converted to "prenex normal form". Where the existential quantifier does not lie within the "scope" of any "universal quantifiers" the "variables" bound by the existential quantifier can simply be replaced by a new "constant" and the existential quantifier removed. Where the existential quantifier does lie within the "scope" of "universal quantifiers" a "Skolem function" needs to be used. ((Domaine indiqué dans la source citée:)) logic
Termes :
- skolemization
- skolemisation
- skolemizing