Skolémisation
Un article de Wikipédia, l'encyclopédie libre.
 |
Cet article est une ébauche concernant les mathématiques.
Vous pouvez partager vos connaissances en l’améliorant. (Comment ?).
|
[modifier] Définition
La skolémisation d'une formule du calcul des prédicats est une transformation de cette formule consistant à remplacer toutes les occurrences du quantificateur existentiel en des occurrences de fonctions.
La version skolémisée d'une formule ne lui est pas équivalente (le langage étant étendu), néanmoins :
- Tout modèle de la formule skolémisée est modèle de la formule initiale.
- Tout modèle de la formule initiale peut être étendu en une sur-structure (par enrichissement du langage avec les symboles de fonction introduits) modèle de la formule skolémisée.
[modifier] Exemple
La formule 
est skolémisée en 
