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

Dernière version du 29 janvier 2024 à 12:33

Fonction introduite pour éliminer les quantificateurs existentiels.

fonction de Skolem

Skolem function

@@ 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.
-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
-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
+==Sources==
-<small>
+[http://gdt.oqlf.gouv.qc.ca/ficheOqlf.aspx?Id_Fiche=17016128  Source : Le grand dictionnaire terminologique  ]
-[http://www.cse.unsw.edu.au/~billw/nlpdict.html   Source : UNWS Natural Language Processing Dictionary ]
+[[Catégorie:GRAND LEXIQUE FRANÇAIS]]