Algorithme d'unification de Herbrand
Avant de voir l'algorithme d'unification de Herbrand, nous devons différencier les formes que peuvent prendre nos formules et fonctions.
Formes normales conjonctives
Lorsque nous avons une conjonction de disjonctions, nous sommes en présence d'une forme normale conjonctive. Toute formule admet une forme normale conjonctive équivalante.
Nous pouvons transformer nos formules en forme normale conjonctive de la manière suivante :
- Transformation des ⇒ par des équivalances p ⇒ q ⇔ ¬p ∨ q
- Ajout de négations pour les atomes avec ¬¬X ⇔ X et les lois de de Morgan (inversion des conjonctions et disjonctions).
- Application de la distributivité de ∧ et ∨ pour obtenir une conjonction (utilisation des ∧) de clauses.
- Renommage des variables si nécessaire.
Formes prénexes
Une formule est de forme prénexe (ou forme normale prénexe) si tous les quantificateurs sont en tête. La suite des quantificateur est le préfixe, et la formule sans quantificateurs est la matrice.
Formes de Skolem
Une formule est de forme de Skolem (ou forme normale de Skolem) si elle est en forme prénexe et ne contient pas de quantificateur existentiel.
Formes clausales
Un littéral est une formule atomique ou la négation d'une formule atomique. Une clause est une disjonction1 de littéraux.
Les variables d'une clause sont implicitement quantifiées universellement (∀) en tête de clause.
Une formule est de forme clausale (ou forme normale clausale) si elle est en forme de Skolem, fermée, et si sa matrice est en forme normale conjonctive propositionnelle.
Terminologie d'Herbrand
Terme clos
Un terme clos est un terme ne contenant pas de variable. L'ensemble des termes clos forme l'univers d'Herbrand. L'univers de Herbrand d'un ensemble de clauses est l'ensemble des termes de base que nous pouvons construire à partir de l'ensemble des termes clos2 que nous retrouvons dans cet ensemble des clauses.
Atome clos
Un atome clos est un atome ne contenant pas de variable. L'ensemble des atomes clos forme la base d'Herbrand.
Interprétation d'Herbrand
Une interprétation de Herbrand est une interprétation dont :
- son domaine est l'univers de Herbrand
- les constantes sont assignées à elles-mêmes
- les variables de l'ensemble de clauses sont remplacées par des éléments de l'univers de Herbrand
Les interprétations d'Herbrand ne diffèrent que par les assignations des prédicats.
Modèle d'Herbrand
Un modèle de Herbrand d'un ensemble de clauses est une interprétation de Herbrand de cet ensemble de clauses qui est un modèle de cet ensemble de clauses.
Algorithme d'unification de Herbrand
Soit S un système d'équations.
Tant que possible répéter
- Sélectionner une équation Eq
- Modifier S selon la forme de Eq comme suit :
- Eq : f(t1,...,tn) = f(u1,...,un)
- Remplacer Eq par les équations t1 = u1,...,tn = un
- Eq : f(t1,...,tm) = f(u1,...,un) avec m ≠ n
- Arrêter avec échec (car le nombre d'arguments des fonctions n'est pas identique).
- Eq : f(t1,...,tm) = g(u1,...,un) avec f ≠ g
- Arrêter avec échec (foncteurs différents).
- Eq : X = X avec X variable
- Eliminer Eq.
- Eq : t = X avec X variable, t non variable
- Remplacer Eq par X = t.
- Eq : X = t avec
- X variable distincte de t
- X apparaît dans S \ {Eq}
- Si X apparaît dans t, arrêter avec échec.
- sinon, remplacer
X par t dans S \ {Eq}
- Eq : f(t1,...,tn) = f(u1,...,un)
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 15/06/2010 gemaakt, de laatste keer de 28/10/2018 gewijzigd
Bron van het afgedrukte document:https://www.gaudry.be/nl/programmation-declarative-unification-herbrand.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.
- ↑ Disjonction : Une disjonction est une ou plusieures relations de type booléen OU.
- ↑ Univers de Herbrand : Quand nous évoquons l'ensemble des termes clos, c'est celui des symboles de fonctions et de constantes du langage du premier ordre considéré.
Referenties
IHDCB337 - Technique d'intelligence artificielle : JM Jacquet, Programmation déclarative
(2009)- IHDCB337 - Technique d'intelligence artificielle : H Toussaint,
Tp
(2009)
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.
