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.
Christoph Quix, Thomas List, René Soiron