Style des formules

Les formules sont affichées en texte
Cette page utilise des fonctions particulières d'affichage de formules (plus d'infos) , vous pouvez choisir entre un affichage mathml, un affichage html, et un affichage texte

Calcul des prédicats : les unifications

Table des matières

Unification

Si nous avons un ensemble d'équations P de la forme  { t1 est SUBSTITUE par s1, ..., tn est SUBSTITUE par sn }  où tout t et tout s sont des termes, nous pouvons parler de problème d'unification; il est peut-être possible de trouver une substitution qui joue le rôle d'unificateur.

Nous pouvons unifier les deux termes t1, t2 ssi ( IL EXISTE  une substitution sigma)   TEL QUE  t1sigma = t2sigma. Le signe « = » correspond ici à une égalité syntaxique.
La substitution sigma porte le nom d'unificateur de t1 et t2.

Nous parlons de l'ensemble des unificateurs (nous noterons U(P) l'ensemble des unificateurs de P), car pouvons avoir plus d'un unificateur pour une même substitution. Nous dirons donc que P est unifiable si U(P) ≠ ∅.

Table des matières Haut

Particularité

Nous dirons d'une substitution alpha qu'elle est plus particulière qu'une autre substitution beta s'il existe une substitution sigma telle que alpha = betasigma. Nous noterons la particularité comme ceci : (alpha  est PLUS PARTICULIER que  beta) .

Table des matières Haut

MGU

Un mgu de deux termes est un unificateur alpha tel que pour tout autre unificateur beta de ces deux termes, beta est plus particulier que alpha

Nous pouvons déterminer le mgu de deux termes gràce à l'algorithme d'unification de Herbrand.

Table des matières Haut

Cette page utilise des fonctions particulières d'affichage de formules (plus d'infos) , vous pouvez choisir entre un affichage mathml, un affichage html, et un affichage texte

Version en cache

22/12/2024 11:08:23 Cette version de la page est en cache (à la date du 22/12/2024 11:08:23) afin d'accélérer le traitement. Vous pouvez activer le mode utilisateur dans le menu en haut pour afficher la dernère version de la page.

Document créé le 10/07/2010, dernière modification le 28/10/2018
Source du document imprimé : https://www.gaudry.be/calcul-predicats-unification-rf-texte.html

L'infobrol est un site personnel dont le contenu n'engage que moi. Le texte est mis à disposition sous licence CreativeCommons(BY-NC-SA). Plus d'info sur les conditions d'utilisation et sur l'auteur.

Notes
  1. ↑ ssi : si et seulement si

  2. ↑a,b most general unifier : correspond à « unificateur le plus général » en français

  3. ↑a,b mgu : “most general unifier” (en français, « unificateur le plus général »)

Table des matières Haut

Références

  1. livre Langue du document :fr IHDCB337 - Technique d'intelligence artificielle : JM Jacquet, Programmation déclarative (2009)
  2. livre Langue du document :fr IHDCB337 - Technique d'intelligence artificielle : H Toussaint, Tp (2009)
  3. livre Langue du document :fr Logique pour l'informatique : Serenella Cerrito, Introduction à la déduction automatique (October 2008)

Ces références et liens indiquent des documents consultés lors de la rédaction de cette page, ou qui peuvent apporter un complément d'information, mais les auteurs de ces sources ne peuvent être tenus responsables du contenu de cette page.
L'auteur de ce site est seul responsable de la manière dont sont présentés ici les différents concepts, et des libertés qui sont prises avec les ouvrages de référence. N'oubliez pas que vous devez croiser les informations de sources multiples afin de diminuer les risques d'erreurs.

Table des matières Haut