Style des formules

Les formules sont affichées en HTML
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

Inhoudsopgave

Unification

Si nous avons un ensemble d'équations P de la forme  { t1 / s1, ..., tn / 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  ∃ une substitution σ : t1σ = t2σ. Le signe « = » correspond ici à une égalité syntaxique.
La substitution σ 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) ≠ ∅.

Inhoudsopgave Haut

Particularité

Nous dirons d'une substitution α qu'elle est plus particulière qu'une autre substitution β s'il existe une substitution σ telle que α = βσ. Nous noterons la particularité comme ceci : α ⊴ β.

Inhoudsopgave Haut

MGU

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

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

Inhoudsopgave 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

Nederlandse vertaling

U hebt gevraagd om deze site in het Nederlands te bezoeken. Voor nu wordt alleen de interface vertaald, maar nog niet alle inhoud.

Als je me wilt helpen met vertalingen, is je bijdrage welkom. Het enige dat u hoeft te doen, is u op de site registreren en mij een bericht sturen waarin u wordt gevraagd om u toe te voegen aan de groep vertalers, zodat u de gewenste pagina's kunt vertalen. Een link onderaan elke vertaalde pagina geeft aan dat u de vertaler bent en heeft een link naar uw profiel.

Bij voorbaat dank.

Document heeft de 10/07/2010 gemaakt, de laatste keer de 28/10/2018 gewijzigd
Bron van het afgedrukte document:https://www.gaudry.be/nl/calcul-predicats-unification-rf-html.html

De infobrol is een persoonlijke site waarvan de inhoud uitsluitend mijn verantwoordelijkheid is. De tekst is beschikbaar onder CreativeCommons-licentie (BY-NC-SA). Meer info op de gebruiksvoorwaarden en de auteur.

Notes
  1. ↑ ssi : si et seulement si

  2. ↑a,b most general unifier : komt overeen met « 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 »)

Inhoudsopgave Haut

Referenties

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

Deze verwijzingen en links verwijzen naar documenten die geraadpleegd zijn tijdens het schrijven van deze pagina, of die aanvullende informatie kunnen geven, maar de auteurs van deze bronnen kunnen niet verantwoordelijk worden gehouden voor de inhoud van deze pagina.
De auteur Deze site is als enige verantwoordelijk voor de manier waarop de verschillende concepten, en de vrijheden die met de referentiewerken worden genomen, hier worden gepresenteerd. Vergeet niet dat u meerdere broninformatie moet doorgeven om het risico op fouten te verkleinen.

Inhoudsopgave Haut