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


(Page créée avec « == en construction == Catégorie:Vocabulary Catégorie:Intelligence artificielle Catégorie:UTexas == Définition == xxxxxxx == Français == xxxxxxx == A... »)
Balise : Éditeur de wikicode 2017
 
Aucun résumé des modifications
Balise : Éditeur de wikicode 2017
Ligne 1 : Ligne 1 :
== 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 construction ==
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.
[[Catégorie:Vocabulary]]
[[Catégorie:Intelligence artificielle]]
[[Catégorie:UTexas]]
 
 
== Définition ==
xxxxxxx


== Français ==
== Français ==
xxxxxxx
'''Skolémisation'''
   
   
== Anglais ==
== Anglais ==
'''Skolemization'''
'''Skolemization'''
the process of eliminating existential quantifiers by replacing them with Skolem constants and Skolem functions.




Ligne 21 : Ligne 14 :


[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]
[[Catégorie:GRAND LEXIQUE FRANÇAIS]]
[[Catégorie:Scotty2]]

Version du 20 mai 2020 à 19:01

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 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.

Français

Skolémisation

Anglais

Skolemization


Source : UTexas Artificial Intelligence Vocabulary

Contributeurs: Imane Meziani, wiki, Sihem Kouache