« Skolémisation » : différence entre les versions


Aucun résumé des modifications
Balise : Éditeur de wikicode 2017
m (Remplacement de texte : « ↵<small> » par «  ==Sources== »)
 
(7 versions intermédiaires par 3 utilisateurs non affichées)
Ligne 1 : Ligne 1 :
== Définition ==
== 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.
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 fait référence au logicien Thoralf Skolem et les fonctions introduites, que l'on peut voir comme des fonctions de choix, sont appelées fonctions de Skolem1.
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 ==
Ligne 11 : Ligne 11 :




<small>
==Sources==
 
[https://fr.wikipedia.org/wiki/Skol%C3%A9misation  Source : Wikipedia]


[https://www.cs.utexas.edu/users/novak/aivocab.html  Source : UTexas Artificial Intelligence Vocabulary]
[https://www.cs.utexas.edu/users/novak/aivocab.html  Source : UTexas Artificial Intelligence Vocabulary]
Ligne 17 : Ligne 19 :


[[Catégorie:GRAND LEXIQUE FRANÇAIS]]
[[Catégorie:GRAND LEXIQUE FRANÇAIS]]
[[Catégorie:Scotty2]]

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

Source : Wikipedia

Source : UTexas Artificial Intelligence Vocabulary

Contributeurs: Imane Meziani, wiki, Sihem Kouache