Als letzten deduktiven Ansatz zum Planen wollen wir das Verfahren von M. Masseron, C. Tollu und J. Vauzeilles [MTV90] vorstellen. Dieses basiert auf Jean-Yves Girards linearer Logik [Gir87], die im wesentlichen ein Gentzen-Kalkül des natürlichen Schließens ist. Jedoch ist eine Anwendung der strukturellen Regeln Abschwächung (engl. weakening) und Kürzung (engl. contraction) nicht erlaubt. Wir haben bereits im Abschnitt 4.7.1 gesehen, daß gerade die Anwendung dieser Regeln zu unerwünschten Ableitungen führte. In diesem Abschnitt wollen wir das in [MTV90] verwendete Fragment der linearen Logik darstellen und aufzeigen, wie damit Planungsprobleme gelöst werden können.
In diesem Fragment sind Formeln entweder die Konstante 1 oder grundinstantiierte Atome oder
zusammengesetzte Ausdrücke der Form , wobei
und
Formeln sind. Der Junktor
entspricht dabei der
im Gentzen-Kalkül des natürlichen Schließens verwendeten Konjunktion
, jedoch ist
im Gegensatz zu
nicht
idempotent. Im weiteren Verlauf dieses Abschnitts werden wir mit
Formeln und mit
Multimengen von
Formeln bezeichnen. Des weiteren werden wir
durch
und
durch
abkürzen. Dabei bezeichnet
die
Multimengenvereinigung.
Der in [MTV90] zum deduktiven Planen verwendete Kalkül ist durch die folgenden Axiome und Ableitungsregeln definiert.
In diesem Kalkül können Formeln weder kopiert noch entfernt werden. Man
beachte außerdem, daß in der Definition der Regel nicht
gefordert wird, wie dies beispielsweise bei der
entsprechenden Einführungsregel für die Konjunktion in einem Gentzen
Kalkül der Fall ist. In einem Kalkül mit
Abschwächung und Kürzung
kann eine solche Forderung immer durch Abschwächung der linken Seiten der
Sequenzen erfüllt werden.
Kommen wir aber jetzt zum Planen zurück und zur Frage, wie Planungsprobleme
in der linearen Logik kodiert und gelöst werden können. Die Aktionen
eines Planungsproblems werden als Theorieaxiome der Form kodiert, wobei
die Vorbedingungen und
die
Effekte der jeweiligen Aktion repräsentieren. Im Eisen und Schwefel Beispiel erhalten
wir die nachfolgend aufgeführten Theorieaxiome für die Aktionen
füge_Schwefel_hinzu, warte und erhitze_Eisen_und_Schwefel.
Um das Beispiel lösen zu können, müssen wir einen linearen logischen
Beweis für die Sequenz finden. Abbildung 4.22
zeigt einen solchen Beweis.
Abbildung 4.22: Ein linearer logischer Beweis für die Sequenz .
Vergleichen wir die in den Abbildungen 4.19(a), 4.20 und 4.22 dargestellten Beweise zur Lösung des Eisen und Schwefel Beispiels, dann zeigt sich unmittelbar, daß die Beweise ineinander übergeführt werden können. Diese Transformationen sind formal in [GHS92] definiert. Dort ist auch die Äquivalenz der drei Kalküle, nämlich der linearen Konnektionsmethode, der Gleichungslogik und der linearen Logik für Planungsprobleme der betrachteten Art bewiesen werden. Da die Gleichungslogik eine Prädikatenlogik 1. Stufe ist und somit eine wohldefinierte und bekannte Semantik besitzt, wird durch ein solches Äquivalenzresultat zum ersten Mal auch eine Standardsemantik für die betrachteten Fragmente der linearen Konnektionsmethode und der linearen Logik definiert.
Wir haben hier nur Planungsprobleme betrachtet, deren Situationsbeschreibungen durch grundinstantiierte Fakten gegeben waren. Jedoch wissen wir aus der Gleichungslogik, daß sich SLDE-Ableitungen von grundinstantiierten Zielklauseln zu SLDE-Ableitungen von allgemeinen (nicht grundinstantiierten) Zielklauseln verallgemeinern (engl. liften) lassen [Höl89]. Somit stellt die Beschränkung auf grundinstantierte Situationsbeschreibungen keine Einschränkung dar. Insbesondere ist es auch möglich, Situationen nur unvollständig zu beschreiben; eine erfolgreiche SLDE-Ableitung liefert dann eine Vervollständigung der Situation. Fragen wir beispielsweise nach der Allgemeingültigkeit der Formel
dh. stellen wir die Frage, ob es möglich ist, aus Schwefel und weiteren
noch unbekannten Stoffen Schwefeleisen herzustellen, dann wird uns ein
entsprechender korrekter und vollständiger Beweiser eine positive
Antwort geben und dabei die Variablen
und
durch
bzw.
ersetzen.
Man beachte, daß eine entsprechende Transformation dieser Anfrage in die
lineare Konnektionsmethode bzw. in die lineare Logik dort jeweils eine
Metaanfrage darstellt, da Situationsbeschreibungen -- wie die oben verwendete
Variable -- in der Gleichungslogik Terme und sowohl in der linearen
Konnektionsmethode wie auch in der linearen Logik Formeln darstellen. Eine
solche Metaanfrage kann dann mit einer der in Abschnitt 4.2.1
behandelten Ansätze formalisiert werden. ZB. besteht einer dieser
Ansätze in der Verwendung einer Logik höherer Stufe. Ein zweiter Ansatz bestand in einer Reifikation von
Aussagen. Im Grunde beruht daher der im Unterabschnitt 4.7.4
behandelte Ansatz zum deduktiven Planen auf solch einer Reifikation des
vorangehenden Ansatzes mit der linearen Konnektionsmethode.
Christoph Quix, Thomas List, René Soiron