« Fonction de Skolem » : différence entre les versions

Version du 22 avril 2021 à 19:53

Fonction introduite pour éliminer les quantificateurs existentiels.

fonction de Skolem

Skolem function

Source : Le grand dictionnaire terminologique

@@ Ligne 1 : / Ligne 1 : @@
-== en construction ==
-[[Catégorie:Vocabulary]]
-[[Catégorie:UNSW]]
 == Définition ==
-xxxxxxx
+Fonction introduite pour éliminer les quantificateurs existentiels.
 == Français ==
-xxxxxxx
+'''fonction de Skolem'''
 == Anglais ==
-'''Skolem functions'''
+'''Skolem function'''
-Universally quantified variables can be handled (and are handled in Prolog) simply by assuming that any variable is universally quantified. Existentially quantified variables must thus be removed in some way. This is handled by a technique called skolemization.
+<small>
-In its simplest form, skolemization replaces the variable with a new constant, called a Skolem constant. For example, the formula:
-exists(y, forall(x, loves(x, y))
-would be encoded as an expression such as
+[http://gdt.oqlf.gouv.qc.ca/ficheOqlf.aspx?Id_Fiche=17016128  Source : Le grand dictionnaire terminologique  ]
-loves(X, sk1),
-where sk1 is a new constant that stands for the object that is asserted to exist, i.e. the person (or whatever) that is loved by every X.
-Quantifier scoping dependencies are shown using new functions called Skolem functions. For example, the formula:
-forall(y, exists(x, loves(x,y))
-would be encoded as an expression such as
-<small>
-[http://www.cse.unsw.edu.au/~billw/nlpdict.html   Source : UNWS Natural Language Processing Dictionary ]
+[[Catégorie:Révision]]