2: Matching

Zu den Aufgaben Folien ansehen Musterlösungen herunterladen

Prolog versucht Anfragen mittels Klauseln (Fakten und Regeln) einer Wissensbasis logisch abzuleiten bzw. zu beweisen.
Dabei wird geprüft ob das Ziel einer Anfrage (die Zielklausel) eine logische Konsequenz der Programmklauseln (Wissensbasis) ist bzw. ob sich eine Anfrage des Benutzers gegeben als Zielklausel auf Grundlage der Programmklauseln beweisen lässt.
Das Prinzip wird automatische Beweisführung (proof search) genannt und beschreibt den Ansatz den Prolog bei der Suche bzw. Beantwortung von Anfragen verfolgt.

Das Matching bzw. die Unifikation

Beim Matching handelt es sich um eine Operation, die zwei Terme miteinander vergleicht bzw. prüft ob diese durch eine geeignete Variablenbelegung gleichgesetzt (unifiziert) werden können.
Das Matching ist ein Teil der automatischen Beweisführung. Es gibt jedoch auch das eingebaute Prädikat (auch Unifikationsoperator genannt) =, welches zwei Terme matcht.

Matchingregel
Zwei Terme matchen genau dann, wenn sie gleich sind oder wenn sie Variablen beinhalten, die so belegt werden können, dass die beiden Terme gleich werden.

Matching einfacher Terme: Variablen

Wenn einer der Terme eine Variable ist, dann kann die Variable mit dem anderen Term belegt werden und beide Terme matchen.
Dies funktioniert unabhängig davon, ob der andere Term einfach oder komplex ist.
Besteht die Anfrage aus mehr als einer elementaren Zielklausel, muss zusätzlich die Variablenbelegung aller Elementarklauseln kompatibel sein.

?- =(mag_spinat(popeye),X).
X = mag_spinat(popeye).
?- X=Y, X=popeye.
X = popeye,
Y = popeye.
?- X=popeye, X=pluto.
false.

Matching: Definition

Seien term1 und term2 zwei Terme.

Wenn term1 und term2 Konstanten sind, matchen sie genau dann, wenn sie das gleiche Atom oder die gleiche Zahl sind.
Wenn term1 eine Variable ist, dann matchen term1 und term2. Die Variable term1 wird dann mit dem Term (term2) instantiiert (analog für den Fall, dass term2 eine Variable ist).
Wenn term1 und term2 komplexe Terme sind, dann matchen sie genau dann, wenn:
1. die Terme den gleichen Funktor und dieselbe Stelligkeit haben und
2. alle korrespondierenden Argumente matchen und
3. die Variablenbelegungen miteinander kompatibel sind.

Wenn keine der drei Gegebenheiten zutrifft, matchen die beiden Terme nicht.

Prolog-Matching vs. Standardunifikation

zyklische Anfrage:

?- vater(X) = X.

In der Auswertung dieser Anfrage unterscheidet sich das Matching von Prolog von der Standardunifikation:

Antwort von Prolog

Die Antwort hängt ab von der Prologimplementierung. Ältere Implementierungen erzeugen Auskünfte wie
Not enough memory to complete query!.
Neuere Implementierungen wie SWI-Prolog matchen die beiden Terme:

?- vater(X) = X. X=vater(X)

Da Matching so zentral für Prolog ist und so häufig passiert ist Prolog optimistisch und erwartet, dass es nicht mit gefährlichen, sprich zyklischen Strukturen gefüttert wird.

Beweisführung: Zusammenfassung

Die Beweisführung in Prolog erfolgt durch die Strategie der Tiefensuche.
Teilziele einer Anfrage werden von links nach rechts bearbeitet.
Für jedes Teilziel wird die erste Klausel (von oben nach unten) ausgewählt.
Ist die Klausel ein Fakt, versucht Prolog die Anfrageklausel mit dem Fakt zu matchen. Gelingt dies, so ist das Teilziel bewiesen.
Ist die Klausel eine Regel, versucht Prolog das Teilziel mit dem Regelkopf zu matchen. Gelingt dies, so versucht Prolog den Regelkörper zu beweisen (der Regelkörper ersetzt das Teilziel). Gelingt dies auch, so ist die Anfrageklausel bewiesen.
Sollte die Beweisführung aufgrund einer unmöglichen Unifikation scheitern, springt Prolog zu dem letzten Punkt zurück, an dem eine Entscheidung getroffen wurde (Backtracking).
Beim Backtracking werden die gemachten Variablenbindungen aufgehoben und nach einer alternativen Klausel gesucht.
Findet Prolog keinen Fakt und keine Regel mit dem die Anfrage bewiesen werden kann, so wird false zurückgegeben.

Beweisführung:

Um eine Zielklausel zu beweisen, versucht Prolog die Klausel mit den in der Wissensbasis gegebenen Fakten und Regelköpfen zu matchen oder zu unifizieren.
Wenn die Anfrage Variablen enthält muss eine gültige Variablenbelegung (matching) gefunden werden.
Das Prinzip der automatischen Beweisführung von Prolog basiert auf dem Prinzip der Unifikation (unification) und des automatischen Rücksetzens (backtracking).

Matching einfacher Terme: Konstanten

Zwei Konstanten matchen genau dann, wenn sie gleich sind.

?- =(popeye,popeye).
true.
?- =(popeye,’Popeye’).
false.
?- =(popeye,’popeye’).
true.
?- =(12,12).
true.
?- =(12,’12’).

Das Prädikat = kann auch in der Infixnotation genutzt werden:

?- regen = schnee.
false.

Matching komplexer Terme

die Terme den gleichen Funktor und dieselbe Stelligkeit haben und
alle korrespondierenden Argumente matchen und
die Variablenbelegungen miteinander kompatibel sind.

?- kill(shoot(gun),Y) = kill(X,stab(knife)).
X = shoot(gun),
Y = stab(knife).
?- kill(shoot(gun), stab(knife)) = kill(X,stab(Y)).
X = shoot(gun),
Y = knife.
?- mag(X,X) = mag(popeye,pluto).
false.

Unifikationsoperator

Neben dem Unifikationsoperator

sonne = regen. =(sonne,regen).

gibt es auch den negierten Unifikationsoperator

sonne \= regen. \=(sonne,regen).

Der Operator \=/2 gelingt genau dann, wenn der Unifikationsoperator =/2 scheitert.

Regeln und die Beweissuche

Angenommen die Wissensbasis enthält eine Regel B :- A (d.h. wenn A gilt, dann gilt auch B.) und es soll B bewiesen werden.

Beweissuche:

B soll bewiesen werden (es erfolgt eine Anfrage zu B).
Matcht ein Fakt oder der Kopf einer Regel aus der Wissensbasis mit B?
Ja und die Regel besagt das B wahr ist, wenn A auch wahr ist.
Kann A bewiesen werden?
Wenn A mit einem Fakt aus der Wissensbasis matcht (d.h. A ist wahr), so folgt, dass auch die Anfrage nach B wahr ist.

Beweisstrategie des Interpreters

Anfrage gilt als zu beweisende Behauptung.
Head-Matching: Anfrage unifiziert mit Kopf einer Klausel (also mit linker Regelseite oder Fakt).
Unifikation liefert Variablenbelegungen.
Klauselrumpf wird bewiesen.
Alternative Lösungen über Backtracking.
Reihenfolge der Suchraumtraversierung: top-down depth-first left-to-right