Nächste Seite: 4.7.6 Planungssysteme (zusammen mit Vorige Seite: 4.7.4 Gleichungslogik

4.7.5 Lineare Logik

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.