Calcul des prédicats : les unifications

Sommaire du document

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) ≠ ∅.

 

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 : α ⊴ β.

 

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.

 

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

 

Réseaux sociaux

Vous pouvez modifier vos préférences dans votre profil pour ne plus afficher les interactions avec les réseaux sociaux sur ces pages.

 

Nuage de mots clés

7 mots clés dont 0 définis manuellement (plus d'information...).

Avertissement

Cette page ne possède pas encore de mots clés manuels, ceci est donc un exemple automatique (les niveaux de pertinence sont fictifs, mais les liens sont valables). Pour tester le nuage avec une page qui contient des mots définis manuellement, vous pouvez cliquer ici.

Vous pouvez modifier vos préférences dans votre profil pour ne plus afficher le nuage de mots clés.

 

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 »)

 

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 (Octobre 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.

 

Historique et modifications de la page

Astuce pour imprimer les couleurs des cellules de tableaux : http://www.gaudry.be/ast-rf-450.html
Aucun commentaire pour cette page

© Ce document issu de l′infobrol est enregistré sous le certificat Cyber PrInterDeposit Digital Numbertection. Enregistrement IDDN n° 5329-13428
Document créé le 10/07/10 02:34, dernière modification le Vendredi 17 Juin 2011, 12:11
Source du document imprimé : http:///www.gaudry.be/calcul-predicats-unification.html
St.Gaudry©07.01.02
Outils (masquer)
||
Recherche (afficher)
Recherche :

Utilisateur (masquer)
Apparence (afficher)
Stats (afficher)
15838 documents
455 astuces.
550 niouzes.
3107 definitions.
447 membres.
8121 messages.

Document genere en :
1,21 seconde

Mises à jour :
Mises à jour du site
Citation (masquer)
Il faut toujours se réserver le droit de rire le lendemain de ses idées de la veille.

Napoléon Bonaparte
 
l'infobrol
Nous sommes le Lundi 26 Juin 2017, 14:20, toutes les heures sont au format GMT+1.00 Heure, heure d'été (+1)