Keine Cache-Version

Caching deaktiviert Standardeinstellung für diese Seite:aktiviert (code LNG204)
Wenn die Anzeige zu langsam ist, können Sie den Benutzermodus deaktivieren, um die zwischengespeicherte Version anzuzeigen.

Algorithme d'unification de Herbrand

Inhaltsverzeichnis

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

Inhaltsverzeichnis 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.

Inhaltsverzeichnis 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.

Inhaltsverzeichnis 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.

Inhaltsverzeichnis Haut

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.

Inhaltsverzeichnis 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 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.

Inhaltsverzeichnis 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(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}

Deutsche Übersetzung

Sie haben gebeten, diese Seite auf Deutsch zu besuchen. Momentan ist nur die Oberfläche übersetzt, aber noch nicht der gesamte Inhalt.

Wenn Sie mir bei Übersetzungen helfen wollen, ist Ihr Beitrag willkommen. Alles, was Sie tun müssen, ist, sich auf der Website zu registrieren und mir eine Nachricht zu schicken, in der Sie gebeten werden, Sie der Gruppe der Übersetzer hinzuzufügen, die Ihnen die Möglichkeit gibt, die gewünschten Seiten zu übersetzen. Ein Link am Ende jeder übersetzten Seite zeigt an, dass Sie der Übersetzer sind und einen Link zu Ihrem Profil haben.

Vielen Dank im Voraus.

Dokument erstellt 15/06/2010, zuletzt geändert 28/10/2018
Quelle des gedruckten Dokuments:https://www.gaudry.be/de/programmation-declarative-unification-herbrand.html

Die Infobro ist eine persönliche Seite, deren Inhalt in meiner alleinigen Verantwortung liegt. Der Text ist unter der CreativeCommons-Lizenz (BY-NC-SA) verfügbar. Weitere Informationen auf die Nutzungsbedingungen und dem Autor.

Aufzeichnungen

  1. ↑ Disjonction : Une disjonction est une ou plusieures relations de type booléen OU.

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

Inhaltsverzeichnis Haut

Referenzen

  1. Buch Sprache des Dokuments:fr IHDCB337 - Technique d'intelligence artificielle : JM Jacquet, Programmation déclarative (2009)
  2. Buch Sprache des Dokuments:fr IHDCB337 - Technique d'intelligence artificielle : H Toussaint, Tp (2009)

Diese Verweise und Links verweisen auf Dokumente, die während des Schreibens dieser Seite konsultiert wurden, oder die zusätzliche Informationen liefern können, aber die Autoren dieser Quellen können nicht für den Inhalt dieser Seite verantwortlich gemacht werden.
Der Autor Diese Website ist allein dafür verantwortlich, wie die verschiedenen Konzepte und Freiheiten, die mit den Nachschlagewerken gemacht werden, hier dargestellt werden. Denken Sie daran, dass Sie mehrere Quellinformationen austauschen müssen, um das Risiko von Fehlern zu reduzieren.

Inhaltsverzeichnis Haut