« Skolémisation » : différence entre les versions
Aucun résumé des modifications |
m (Remplacement de texte : « ↵<small> » par « ==Sources== ») |
||
| (Une version intermédiaire par un autre utilisateur non affichée) | |||
| Ligne 2 : | Ligne 2 : | ||
En logique mathématique, la skolémisation d’une formule du calcul des prédicats est une transformation de cette formule, qui, dans le cas d’une forme prénexe, consiste à éliminer toutes les occurrences de quantificateur existentiel en utilisant de nouveaux symboles de fonction (un par quantification existentielle), tout en conservant la satisfaisabilité de la formule. | En logique mathématique, la skolémisation d’une formule du calcul des prédicats est une transformation de cette formule, qui, dans le cas d’une forme prénexe, consiste à éliminer toutes les occurrences de quantificateur existentiel en utilisant de nouveaux symboles de fonction (un par quantification existentielle), tout en conservant la satisfaisabilité de la formule. | ||
La terminologie | La terminologie provient du nom du logicien Thoralf Skolem et les fonctions introduites, que l’on peut voir comme des fonctions de choix, sont appelées fonctions de Skolem. | ||
== Français == | == Français == | ||
'''Skolémisation''' | '''Skolémisation''' | ||
| Ligne 10 : | Ligne 11 : | ||
==Sources== | |||
[https://fr.wikipedia.org/wiki/Skol%C3%A9misation Source : Wikipedia] | [https://fr.wikipedia.org/wiki/Skol%C3%A9misation Source : Wikipedia] | ||
| Ligne 18 : | Ligne 19 : | ||
[[Catégorie:GRAND LEXIQUE FRANÇAIS]] | [[Catégorie:GRAND LEXIQUE FRANÇAIS]] | ||
Dernière version du 28 janvier 2024 à 12:19
Définition
En logique mathématique, la skolémisation d’une formule du calcul des prédicats est une transformation de cette formule, qui, dans le cas d’une forme prénexe, consiste à éliminer toutes les occurrences de quantificateur existentiel en utilisant de nouveaux symboles de fonction (un par quantification existentielle), tout en conservant la satisfaisabilité de la formule.
La terminologie provient du nom du logicien Thoralf Skolem et les fonctions introduites, que l’on peut voir comme des fonctions de choix, sont appelées fonctions de Skolem.
Français
Skolémisation
Anglais
Skolemization
Sources
Contributeurs: Imane Meziani, wiki, Sihem Kouache
