voriges Kapitel | Startseite | Inhalt | nächstes Kapitel

© 2001 François Bry
Dieses Lehrmaterial wird ausschließlich zur privaten Verwendung angeboten. Eine nichtprivate Nutzung (z.B. im Unterricht oder eine Veröffentlichung von Kopien oder Übersetzungen) dieses Lehrmaterials bedarf der Erlaubnis des Autors.


1. Lineare Resolutionsbeweise

Lineare Resolutionsbeweise: Variablenfreier Fall

Die Aussage gehe_schwimmen kann unter Anwendung des Programms P9 wie folgt bewiesen werden, wobei jede Liste einem Zustand im Beweis entspricht:
< gehe_schwimmen > < sonne_scheint, habe_zeit > < habe_zeit > < arbeite_nicht > < wochenende > < samstag > < >
Ist die Liste leer, so ist die ursprüngliche Anfrage, hier gehe_schwimmen, bewiesen.
Offenbar führen nicht alle solche Sequenzen zu einem Beweis:
< gehe_schwimmen > < es_regnet, arbeite_nicht >
kann unter Anwendung von P9 nicht zur leeren Liste führen, weil es_regnet weder im Kopf einer Regel noch als Faktum in P9 vorkommt.
Beweise wie in den vorangehenden Beispielen heißen lineare Resolutionsbeweise.
Für variablenfreie Anfragen und Programme können die linearen Beweise bezüglich eines variablenfreien und negationsfreien Programms P wie folgt formalisiert werden.

Sei A = A1, ..., An eine negationsfreie variablenfreie Anfrage.

  • Ist A1 :- L1, ..., Lm eine Regel in P, so ist A1, A2, ..., An ---> L1, ..., Lm, A2, ..., An ein Resolutionsschritt aus A = A1, ..., An bezüglich P.
  • Ist A1 ein Faktum in P, so ist A1, A2, ..., An ---> A2, ..., An ein Resolutionsschritt aus A = A1, ..., An bezüglich P.
Ein linearer Resolutionsbeweis von einer negationsfreien und variablenfreien Anfrage A bezüglich eines negationsfreien und variablenfreien Programms P ist eine Sequenz A0 ---> A1 ---> . . . ---> Ak wobei A0 = A ist, Ak ist die leere Anfrage, und für alle i von 1 bis k ist Ai-1 ---> Ai ein Resolutionsschritt.
Bemerkung: Diese Definition legt die Auswahl des "resolvierten" Atoms aus der Anfrage fest.

Unifikationsalgorithmus

Im allgemeinen Fall von negationsfreien Anfragen und Programmen mit Variablen müssen die Variablen gebunden werden, um Atome aus der Anfrage und Regelköpfe zu "unifizieren".
Seien p(t1, ..., tn) und p(s1, ..., sn) zwei Atome.

Algorithmus zur Unifikation von p(t1, ..., tn) und p(s1, ..., sn):

  1. Initialisierung:
    GS := {t1 = s1, ..., tn = sn}
  2. Reduktion:
    Solange Reduktionsschritte (s. unten) anwendbar sind, wende einen anwendbaren Reduktionsschritt an.
  3. Ergebnis:
    Falls GS den Wert "scheitert" hat, sind p(t1, ..., tn) und p(s1, ..., sn) nicht unifizierbar. Andernfalls ist GS ein allgemeinster Unifikator der beiden Atome.
Reduktionsschritte:
  1. {t = X} U G  --->  {X = t} U G
    falls t keine Variable ist.
  2. {X = X} U G  ---> G
  3. {f(u1,...,uk) = g(v1,...,vl)} U G  --->  "scheitert"
    falls f verschieden von g ist oder k verschieden von l (klein L) ist.
  4. {f(u1,...,uk) = f(v1,...,vk)} U G  --->  {u1 = v1, ..., uk = vk)} U G
  5. {X = t} U G  --->  {X = t} U G'
    falls die Variable X in G vorkommt. Dabei entsteht G' aus G durch Ersetzen von jedem Vorkommen der Variablen X durch den Term t.
Bemerkungen:
  1. Der obige Unifikationsalgorithmus leistet den "Occur-Check"-Test nicht.
  2. Es gibt effizientere Versionen des Unifkationsalgorithmus -- mit oder ohne "Occur-Check"-Test.
Eine Substitution sigma = {X1 = t1, ..., Xn = tn} definiert eine Funktion über Terme, Atome und im Allgemeinen Ausdrücke, die jeden Ausdruck A auf den Ausdruck abbildet, der sich aus A ergibt, wenn alle Vorkommen einer Variablen Xi durch ti ersetzt werden.
Ist R eine Regel oder ein Faktum in einem Programm P, so nennt man Variante von R die Regel oder das Faktum, das sich aus R ergibt, wenn die in R vorkommenden Variablen konsistent durch andere ersetzt werden, so daß keine zwei Variablen von R durch die gleiche Variable ersetzt werden.

Lineare Resolutionsbeweise: Allgemeiner Fall

Sei P ein negationsfreies Programm und A = A1, ... , An eine negationsfreie Anfrage.
Ist R = B :- L1, ..., Lm eine Variante einer Regel in P, die keine gemeinsame Variable mit A besitzt, und ist sigma ein allgemeinster Unifikator von A1 und B, so ist A1, A2, ..., An --->R / sigma   sigma(L1), ..., sigma(Lm), sigma(A2), ..., sigma(An) ein Resolutionsschritt aus A bezüglich P.
Ist B eine Variante eines Faktums in P, die keine gemeinsame Variable mit A besitzt, und ist sigma ein allgemeinster Unifikator von A1 und B, so ist
A1, A2, ..., An --->B / sigma sigma(A2), ..., sigma(An) ein Resolutionsschritt aus A bezüglich P.

Ein linearer Resolutionsbeweis von einer negationsfreien Anfrage A bezüglich eines negationsfreien Programms P ist eine Sequenz

A0 --->R1 / sigma-1 A1 --->R2 / sigma-2 . . . --->Rk / sigma-k Ak
so daß
  1. A0 = A ist,
  2. Ak ist die leere Anfrage,
  3. für alle i von 1 bis k ist Ai-1 --->Ri / sigma-i Ai ein Resolutionsschritt, und
  4. Ri ist eine Variante einer Regel oder eines Faktums im Programm P, die keine gemeinsame Variable besitzt mit der Sequenz
    A0 --->R1 / sigma-1 A1 --->R2 / sigma-2 . . . --->Ri-1 / sigma-i-1 Ai-1
Die letzte Bedingung ist notwendig, damit die Allgemeinheit des Beweises nicht eingeschränkt wird, wie das folgende Beispiel zeigt:
10
p(X,Y) :- q(X), r(Y). q(Y) :- s(Y). s(a). r(b).
Ist
A0 --->R1 / sigma-1 A1 --->R2 / sigma-2 . . . --->Rk / sigma-k Ak
ein linearer Resolutionsbeweis von einer negationsfreien Anfrage A bezüglich eines negationsfreien Programms P, so bilden die Bindungen aus der Komposition von Substitutionen sigma-1 o ... o sigma-k, die Variablen von A binden, eine Antwort.
Die linearen Resolutionsbeweise sind der Auswertung von PROLOG-Programmen treu. Der Keller der abstrakten Maschine einer Implementierung von PROLOG enthält zu jeder Zeit eine Sequenz von Resolutionsschritte.

zum Seitenanfang

Lineare Resolutionsbeweise (1)


Variablenfreier Fall:

Ein linearer Resolutionsbeweis von einer negationsfreien und variablenfreien Anfrage A bezüglich eines negationsfreien und variablenfreien Programms P ist eine Sequenz A0 ---> A1 ---> . . . ---> Ak wobei A0 = A ist, Ak ist die leere Anfrage, und für alle i von 1 bis k ist Ai-1 ---> Ai ein Resolutionsschritt.

Unifikationsalgorithmus:

Seien p(t1, ..., tn) und p(s1, ..., sn) zwei Atome.

Algorithmus zur Unifikation von p(t1, ..., tn) und p(s1, ..., sn):

  1. Initialisierung:
    GS := {t1 = s1, ..., tn = sn}
  2. Reduktion:
    Solange Reduktionsschritte (s. unten) anwendbar sind, wende einen anwendbaren Reduktionsschritt an.
  3. Ergebnis:
    Falls GS den Wert "scheitert" hat, sind p(t1, ..., tn) und p(s1, ..., sn) nicht unifizierbar. Andernfalls ist GS ein allgemeinster Unifikator der beiden Atome.

Lineare Resolutionsbeweise (2)


Allgemeiner Fall:

Ein linearer Resolutionsbeweis von einer negationsfreien Anfrage A bezüglich eines negationsfreien Programms P ist eine Sequenz
A0 --->R1 / sigma-1 A1 --->R2 / sigma-2 . . . --->Rk / sigma-k Ak
so daß
  1. A0 = A ist,
  2. Ak ist die leere Anfrage,
  3. für alle i von 1 bis k ist Ai-1 --->Ri / sigma-i Ai ein Resolutionsschritt, und
  4. Ri ist eine Variante einer Regel oder eines Faktums im Programm P, die keine gemeinsame Variable besitzt mit der Sequenz
    A0 --->R1 / sigma-1 A1 --->R2 / sigma-2 . . . --->Ri-1 / sigma-i-1 Ai-1

Beweisbäume


Das folgende ist ein linearer Resolutionsbeweis:
p ---> q, r, s ---> s, r, s ---> r, s ---> t, u, s ---> u, s ---> s --->
Er kann wie folgt als Baum dargestellt werden:
p | +-----------+-----------+ | | | q r s | | s +---+---+ | | t u

3. Auswahl einer Klausel, Auswahl eines Literals

Die Definition der linearen Resolutionsbeweise legt die Reihenfolge fest, mit der die Atome einer Anfrage "wegresolviert" werden: sie werden von links nach rechts bearbeitet, und die beim letzten Resolutionsschritt hinzugefügten Atome werden als erste berücksichtigt.

Bei der Suche nach einem linearen Resolutionsbeweis werden die Fakten und Regeln des Programms in der Reihenfolge probiert, wie sie im Programm stehen.

Diese feste Reihenfolge gilt für alle PROLOG-Systeme.

Sowohl die Reihenfolge der Bearbeitung der Anfrageatome als auch der Programmregeln und -fakten kann durch Veränderung der Aufschreibreihenfolge beeinflußt werden, was in manchen Fällen vorteilhaft ist.

12
verbunden(X,Y) :- kante(X,Y). verbunden(X,Y) :- kante(X,Z), verbunden(Z,Y). kante(k1,k2). kante(k2,k3). kante(k3,k1).
Programm P12 spezifiziert die transitive Hülle verbunden der binären Relation kante. Auf die Anfrage verbunden(U,V) liefert es nur fünf der neun möglichen Antworten, weil es in eine Endlosschleife gerät, in der drei dieser Antworten ständig wiederholt werden.
13
verbunden(X,Y) :- kante(X,Y). verbunden(X,Y) :- verbunden(Z,Y), kante(X,Z). kante(k1,k2). kante(k2,k3). kante(k3,k1).
Programm P13 ist dem Programm P12 ähnlich, zumindest was die "deklarative Semantik" angeht. Es unterscheidet sich nur dadurch, daß die Atome im Rumpf der zweiten Regel vertauscht sind. Bezüglich der Anfrage verbunden(U,V) verhält es sich aber anders: Es berechnet zuerst alle neun Antworten, wiederholt dies dann aber unendlich oft.
14
verbunden(X,Y) :- verbunden(Z,Y), kante(X,Z). verbunden(X,Y) :- kante(X,Y). kante(k1,k2). kante(k2,k3). kante(k3,k1).
Programm P14 ist eine weitere Spezifikation der transitiven Hülle verbunden der binären Relation kante, die einen anderen Ablauf bei der Auswertung der Anfrage verbunden(U,V) hervorbringt: keine Verbindung wird berechnet und die Berechnung verfällt sofort in eine unendliche Schleife.

zum Seitenanfang

Auswahl einer Klausel, Auswahl eines Literals


  • Definition der linearen Resolutionsbeweise --> Reihenfolge mit der Atome einer Anfrage "wegresolviert" werden
  • Suche nach Resolutionsbeweis: Fakten und Regeln werden in der Reihenfolge, in der sie im Programm stehen probiert
  • Diese feste Reihenfolge gilt für alle PROLOG-Systeme
  • Änderung der Bearbeitungsreihenfolge durch Veränderung der Aufschreibreihenfolge möglich

4. Das "Cut" zur Steuerung der Suche

PROLOG bietet ein sogenanntes nichtlogisches Konstrukt, das "Cut" (geschrieben !), zur Steuerung der Suche.
Dieses Beispiel liefert eine Gelegenheit, das PROLOG-Systemprädikat op zu erläutern. Das Systemprädikat op dient der Deklaration von Operatoren, d.h. von Relationssymbolen, die mit Sonderzeichen bezeichnet werden, oder Post- oder Infix geschrieben werden. Es wird wie folgt verwendet:
:- op(Präzedenz, Klammerung, Name)
Die Präzedenz ist eine natürliche Zahl. Je größer sie ist, desto schwächer bindet der Operator. Die Deklaration
:- op(21, yfx, +). :- op(31, yfx, *).
bewirken, daß die Eingabe 2 + 3 * 5 als (2 + 3) * 5 gelesen wird.

Bei Infix-Operatoren, die notwendigerweise binäre Relationssymbole sind, ist die Klammerung eines der Kürzel xfx, xfy, yfx und yfy. Bei Präfix-Operatoren, die notwendigerweise unäre Relationssymbole sind, ist die Klammerung eines der Kürzel fx und fy. Bei Postfix-Operatoren, die notwendigerweise unäre Relationssymbole sind, ist die Klammerung eines der Kürzel xf und yf. Ein x bedeutet, daß der Operator an dieser Stelle nicht ungeklammert vorkommen darf. Ein y bedeutet dagegen, daß der Operator an dieser Stelle auch ohne Klammern wieder vorkommen darf, und dann so behandelt wird als sei er geklammert.

:- op(35, xfx, **). yes. :- X = 2 ** 3 ** 5. syntax error: bracket necessary | X = 2 ** 3 ** 5. | ^ here :- op(35, xfy, **). yes. :- X = 2 ** 3 ** 5. X = 2 ** 3 ** 5 yes. :- A ** B = 2 ** 3 ** 5. A = 2 B = 3 ** 5 yes. :- op(35, yfx, **). yes. :- A ** B = 2 ** 3 ** 5. A = 2 ** 3 B = 5 yes. :- op(60, fx, nicht). yes. :- A = nicht nicht p. syntax error: bracket necessary | A = nicht nicht p. | ^ here :- op(60, fy, nicht). yes. :- A = nicht nicht p. A = nicht nicht p yes. :-
fail ist in PROLOG ein 0-stelliges Relationssymbol, das nicht bewiesen werden kann, also immer scheitert. Die Kombination "Cut-Fail" ist besonders interessant.
Die "Cut-Fail"-Kombination erinnert an eine Negation (siehe unten). Das folgende Programm P21, in dem der Rumpf der ersten Klausel durch eine Negation ersetzt wurde, verhält sich aber anders als P20: Der Aufruf variablenfrei(f(X)) scheitert mit P20, ist aber mit P21 erfolgreich, weil die erste Klausel von P21 in dem Fall erfolgreich ist.
Es stellt sich oft die Frage, ob ein Programm mit oder ohne Cuts geschrieben werden soll. Die Cuts haben den Nachteil, keine deklarative Auslegung zu haben. Sie sind aber oft aus Effizienzgründen unverzichtbar (siehe die Beispiele am Anfang des Absatzes).
Um diese Frage zu beantworten, hilft es oft zu überlegen, ob das Programm als "Generator" oder als "Test" verwendet werden soll. Das folgende Beispiel veranschaulicht die Begriffe:
Um Elemente der Liste zu generieren, ist member, also ohne Cut, anzuwenden. Soll aber nur getestet werden, ob ein bereits bekanntes Objekt in einer (bereits bekannten) Liste vorkommt, dann kann das effizientere is_member verwendet werden.

zum Seitenanfang

Das "Cut" zur Steuerung der Suche


  • "Cut": nichtlogisches Konstrukt zur Steuerung der Suche (geschrieben !)
  • op: PROLOG-Systemprädikat zur Deklaration von Operatoren
  • fail: 0-stelliges Relationssymbol, das nicht bewiesen werden kann

5. Probleme der Negation

Die Negation von PROLOG, \+ oder not geschrieben, wird folgendermaßen ausgewertet: Um eine Anfrage der Form \+ A auszuwerten, wird zunächst in einer "Nebenrechnung" die Anfrage A ausgewertet. Scheitert diese Auswertung in der "Nebenrechnung", so gilt \+ A als bewiesen. Wird dagegen in der Nebenrechnung ein Beweis für A gefunden, dann scheitert die Auswertung von \+ A.

zum Seitenanfang

Probleme der Negation


Auswerten einer Negation (z.B. \+ A):
  • in "Nebenrechnung" Anfrage A auswerten
  • A scheitert --> \+ A gilt als bewiesen
  • A wird bewiesen --> \+ A scheitert
--> Diese Auslegung hat manchmal unerwünschte Folgen, denn die prozedurale Definition der Negation in PROLOG ermöglicht nicht, daß ein negatives Literal Bindungen für Variablen berechnet.

PROLOG und die Logikprogrammierung


  • PROLOG ist die bekannteste Sprache der Logikprogrammierung. Die Logikprogrammierung umfaßt aber mehr als nur PROLOG.
  • Besonderheiten von PROLOG sind u. a. die Auswahlfunktionen zur Selektion der Regeln und Fakten aus dem Programm und des Literals aus der Anfrage, sowie die Tiefensuche.
  • PROLOG hat sogenannte nichtlogische Konstrukte, die nicht unumstriten sind, darunter !, assert, retract.
  • Obwohl kritisiert, ist PROLOG sehr beliebt und wird häufig, auch in der Industrie, für das sogenannte "rapid prototyping" verwendet. Es gibt zahlreiche Erfolgsgeschichten über den industriellen Einsatz von PROLOG.
voriges Kapitel | Startseite | Inhalt | nächstes Kapitel

Letzte Änderung: 18. August 1998

Valid
	     XHTML 1.0!