Forme normale de skolem

Forme normale de skolem

Skolémisation

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), ce de façon à conserver la satisfaisabilité de la formule.

L'expression 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 Skolem.[1]

Intuitivement, si on a une formule du type \forall x\,\exists y\, P(x, y) on peut se dire que pour chaque x il existe (au moins) un y tel que P(x,y) est vrai, on peut donc supposer qu'il y a une fonction f(x) qui nous fournit un "bon" y pour chaque x. Ceci nous permet de réécrire la formule comme \forall x\, P(x, f(x)).

Il est plus simple de décrire la skolémisation pour une formule sous forme prénexe, c'est-à-dire avec tous les quantificateurs au début (en appliquant les équivalences connues on arrive toujours à le faire). Dans ce cas, chaque occurrence d'une variable y quantifiée existentiellement est remplacée par un terme f(x_1, \ldots, x_n)x_1, \ldots, x_n sont les variables quantifiées universellement dont le quantificateur apparaît avant celui de y. S'il n'y aucun quantificateur universel avant \exists y, f sera une fonction 0-aire, c-à-d une constante. Pour chaque variable à skolémiser il faut choisir un nouveau nom de fonction qui n'apparait pas déjà dans la formule.

La formule obtenue, qui est une formule prénexe n'ayant que des quantificateurs universelles en tête, est parfois dite sous forme normale de Skolem. Il n'y a pas unicité (même au noms des symboles de fonctions près, et à équivalence près de la partie propositionnelle) de la forme normale de Skolem d'une formule donnée.

Sommaire

Exemples

  1. La formule \forall x \exists y \forall z P(x,y,z) n'est pas sous forme normale de Skolem car elle contient un quantificateur existentiel. La skolémisation remplace y par f(x), où f est une nouvelle fonction et supprime le quantificateur \exists y. La formule résultante est \forall x \forall z P(x,f(x),z).
  2. La formule \forall x\, \exists y\, (\mathrm{Etudiant}(x) \to (\mathrm{Fac}(y) \land \mathrm{Inscrit}(x, y))) peut être skolémisée en \forall x (\mathrm{Etudiant}(x) \to (\mathrm{Fac}(f(x)) \land \mathrm{Inscrit}(x, f(x)))
  3. La formule \forall x\,  \exists y\,  \forall z\, \exists u\, (R(x,y) \land S(y, z, u)) peut être skolémisée en \forall x\, \forall z\, (R(x,f(x)) \land S(f(x), z, g(x, z))) (y dépend uniquement de x, u dépend de x et de z)
  4. La formule \exists x\, \forall y\, (x > y) deviendra \forall y\, (c > y), où c est une constante d'individu.

Propriétés

La version skolémisée d'une formule ne lui est pas équivalente (le langage étant étendu), néanmoins :

Tout modèle de la formule skolémisée est modèle de la formule initiale.
Tout modèle de la formule initiale peut être étendu en une sur-structure (par enrichissement du langage avec les symboles de fonction introduits) modèle de la formule skolémisée.

Utilisation

En raisonnement automatique et en programmation logique (p.ex. dans le langage Prolog) on utilise fréquemment le principe de résolution de Robinson. Or cette règle d'inférence ne s'applique que sur des formules dont les variables sont toutes quantifiées universellement (en fait sur des clauses). Il faut donc passer par une étape de skolémisation avant de pouvoir appliquer la résolution.

Annexes

Articles connexes

Bibliographie

  • (en) Dirk van Dalen, Logic and Structure, Third edition, ed. Springer-Verlag, Berlin Heidelberg, 1994. Chapitre "3.4 Skolem Functions or How to Enrich Your Language", pp. 136-142 (de la 3e édition). ISBN 3-540-57839-0 et ISBN 0-387-57839-0.

Notes et références

  1. D. van Dalen, opp.cit., p.136 : The idea of enriching the language by the introduction of extra function symbols, which take the role of choice functions, goes back to Skolem.
  • Portail de la logique Portail de la logique
Ce document provient de « Skol%C3%A9misation ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Forme normale de skolem de Wikipédia en français (auteurs)

Игры ⚽ Поможем написать реферат

Regardez d'autres dictionnaires:

  • Forme Normale De Skolem — Skolémisation 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… …   Wikipédia en Français

  • Forme normale de Skolem — Skolémisation 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… …   Wikipédia en Français

  • Thoralf Skolem — Thoralf Albert Skolem (23 mai 1887 23 mars 1963) était un mathématicien et logicien norvégien. Il est particulièrement connu pour les travaux en logique mathématique et théorie des ensembles qui portent à présent son nom, comme le théorème de… …   Wikipédia en Français

  • Skolémisation — 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… …   Wikipédia en Français

  • Skolemisation — Skolémisation 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… …   Wikipédia en Français

  • Projet:Mathématiques/Liste des articles de mathématiques — Cette page n est plus mise à jour depuis l arrêt de DumZiBoT. Pour demander sa remise en service, faire une requête sur WP:RBOT Cette page recense les articles relatifs aux mathématiques, qui sont liés aux portails de mathématiques, géométrie ou… …   Wikipédia en Français

  • Liste des articles de mathematiques — Projet:Mathématiques/Liste des articles de mathématiques Cette page recense les articles relatifs aux mathématiques, qui sont liés aux portails de mathématiques, géométrie ou probabilités et statistiques via l un des trois bandeaux suivants  …   Wikipédia en Français

  • CORPS (mathématiques) — La structure de corps n’est en fait qu’un cas particulier de la structure plus générale d’anneau [cf. ANNEAUX ET ALGÈBRES]; en plus des axiomes généraux, on stipule que le groupe multiplicatif des éléments inversibles est le complémentaire de 0.… …   Encyclopédie Universelle

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”