Algorithme d'unification de Herbrand

Table des matières

Avant de voir l'algorithme d'unification de Herbrand, nous devons différencier les formes que peuvent prendre nos formules et fonctions.

Table des matières Haut

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.

Table des matières Haut

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.

Table des matières Haut

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.

Table des matières Haut

Formes clausales

Un littéral est une formule atomique ou la négation d'une formule atomique. Une clause est une disjonction¹ 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.

Table des matières Haut

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 clos² 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.

Table des matières Haut

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(t₁,...,t_n) = f(u₁,...,u_n)
  - Remplacer Eq par les équations t₁ = u₁,...,t_n = u_n
- Eq : f(t₁,...,t_m) = f(u₁,...,u_n) avec m ≠ n
  - Arrêter avec échec (car le nombre d'arguments des fonctions n'est pas identique).
- Eq : f(t₁,...,t_m) = g(u₁,...,u_n) 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}

Version en cache

21/11/2024 10:03:03 Cette version de la page est en cache (à la date du 21/11/2024 10:03:03) 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 15/06/2010, dernière modification le 28/10/2018
Source du document imprimé : https://www.gaudry.be/programmation-declarative-unification-herbrand.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

↑ 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é.

Table des matières Haut

Références

IHDCB337 - Technique d'intelligence artificielle : JM Jacquet, Programmation déclarative (2009)
IHDCB337 - Technique d'intelligence artificielle : H Toussaint, Tp (2009)

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