Nächste Seite: 4.7.4 Gleichungslogik Vorige Seite: 4.7.2 Der Situationskalkül

4.7.3 Lineare Konnektionsmethode

1986 schlug einer der Autoren vor, zum Planen eine Variante der Konnektionsmethode zu verwenden [Bib86]. Die Modifikation bestand darin, nur sogenannte lineare Beweise zuzulassen, in denen jedes Literal höchstens einmal konnektiert sein darf. Wir wollen diese Idee am Eisen und Schwefel Beispiel illustrieren. Wir erinnern uns, daß in der Ausgangssituation dieses Beispiels lediglich Eisen vorhanden ist. In der linearen Konnektionsmethode wird dies durch ein Atom Fe repräsentiert. Zusätzlich dazu geben wir ein weiteres Atom an. Aufgabe des Prädikats Zustand wird es sein, auf der Argumentposition die Liste der Aktionen zu kodieren, die ausgeführt wurden, um ein Ziel zu erreichen. Dabei repräsentiert die Konstante die leere Liste. Es spielt somit die Rolle eines Speichers, in dem die Antwortsubstitution im Sinne der logischen Programmierung (siehe zB. [Llo84]) abgelegt wird. Zusammen erhalten wir

Die Aktionen füge_Schwefel_hinzu, warte und erhitze_Eisen_und_Schwefel werden wie folgt repräsentiert.

Das Ziel, nämlich Schwefeleisen zu erhalten, wird durch

angegeben. Hierbei haben wir die erforderliche Aktionenfolge füge_Schwefel_hinzu, warte und erhitze_Eisen_und_Schwefel im Zustandsliteral bereits mit angegeben; wäre sie uns nicht bekannt, würden wir diesen Term durch eine Variable ersetzen, die erst durch den nachfolgenden Beweis durch genau diesen Term ersetzt würde (siehe zu dieser Bemerkung die Diskussion am Ende des Abschnitts 4.7.5). Die Aufgabe besteht nun darin, nachzuweisen, daß (4.20) logisch aus (4.18) und (4.19) folgt, dh. daß

allgemeingültig ist. Dazu beseitigen wir die Quantoren, transformieren (4.21) in Matrixform und können dann einen linearen Konnektionsbeweis angeben, so wie das in Abbildung 4.19(a) geschehen ist.

Abbildung 4.19: (a) Ein linearer Konnektionsbeweis für (4.21); jedes Literal ist höchstens einmal konnektiert. (b) Ein Konnektionsbeweis für (4.22); die Literale und sind zweimal konnektiert.

Man beachte, daß es keinen linearen Konnektionsbeweis für die Aussage

gibt. Ein möglicher Konnektionsbeweis für (4.22) ist in Abbildung 4.19(b) angegeben. Allerdings ist dieser Beweis nicht linear, da die Literale und zweimal konnektiert sind. Wenn wir diesen Beweis mit der Ableitung in Abbildung 4.17 vergleichen, dann korrespondieren die zweifach konnektierten Literale exakt mit der zweimaligen Anwendung der Abschwächung in Abbildung 4.17.

Aber wieso löst die lineare Konnektionsmethode das Eisen und Schwefel Beispiel sowie ia. auch das Rahmenproblem? Die entscheidende Idee ist, daß Literale in der linearen Konnektionsmethode als Ressourcen angesehen werden. Literale werden verbraucht, indem sie konnektiert werden, und sie werden als Konsequenz einer Aktion generiert, sobald die Vorbedingungen der Aktion erfüllt sind. Betrachten wir zur Illustration dieser Beobachtung noch einmal Abbildung 4.19. Sobald mit konnektiert ist, kann an keiner weiteren Konnektion mehr beteiligt sein; ist verbraucht. Sobald die Vorbedingungen , und der erhitze_Eisen_und_Schwefel Aktion erfüllt sind, kann die Aktion ausgeführt werden, und wir erhalten die neuen Ressourcen und . Sowohl im Situationskalkül wie auch in der normalen Konnektionsmethode oder einem Gentzen-Kalkül werden Literale nicht als Ressourcen, sondern als Eigenschaften angesehen und können folglich mehrmals an Konnektionen beteiligt sein.

In dem hier betrachteten Planungsbeispiel sind sowohl die Vorbedingungen wie auch die Effekte von Aktionen jeweils durch -- wie sich später noch herausstellen wird -- nicht-idempotente Konjunktionen definiert. Wir werden hier nur solche Planungsproblem betrachten. Die lineare Konnektionsmethode ist apriori jedoch nicht auf solche Formelklassen beschränkt, sondern erlaubt alllgemeine prädikatenlogische Ausdrücke als Vor- und Nachbedingungen von Aktionen.

Als einer der Autoren 1986 die lineare Konnektionsmethode vorstellte, wurde er heftig kritisiert, ua. weil er keine Standardsemantik für diese Methode angeben konnte (siehe die Diskussion in [Bib88c]). Es gibt zwar inzwischen Nicht-Standardsemantiken für die Lineare Konnektionsmethode [BdCFH89], aber auch eine Standardsemantik, die wir im nächsten Unterabschnitt angeben wollen.