gif gif up gif contents index
Nächste Seite: 4.7.3 Lineare Konnektionsmethode Vorige Seite: 4.7.1 Allgemeine Prädikatenlogik

4.7.2 Der Situationskalkül

Wie wir im letzten Unterabschnitt gesehen haben, ist eine naive Modellierung von Planungsproblemen mit Hilfe der Prädikatenlogik nicht adäquat. Vielleicht hätten wir die in (4.11) vorkommenden Atome mit der Situation markieren sollen, in der sie gelten. Beispielsweise hätten wir Fe und S mit Situation und FeS mit Situation markieren können, womit dann deutlich würde, daß durch Erhitzen von Eisen und Schwefel in Situation Schwefeleisen in entsteht.

Das Markieren von Aussagen mit den Situationen, in denen sie gelten, ist die zentrale Idee, auf der der von John McCarthy und Pat Hayes [McC63, MH69] entwickelte Situationskalkül beruht. Formal führen McCarthy und Hayes sogenannte Fluenten ein. Ein Fluent ist ein Prädikats- oder Funktionszeichen, bei dem ein Argument für eine Situation steht. Handelt es sich um ein Prädikatszeichen, dann sprechen wir von einem propositionalen Fluent, während wir im Falle eines Funktionszeichens von einem Situationsfluent sprechen, dessen Wertebereich wiederum als die Menge der Situationen angenommen wird.

Im Situationskalkül läßt sich die Ausgangssituation des Eisen und Schwefel Beispiels durch den propositionalen Fluent

beschreiben, wobei Fe ein Prädikatszeichen und eine Konstante ist. Das Situationsfluent bezeichnet die Situation, die durch Anwendung der Aktion in Situation erhalten wird. Damit lassen sich die Aktionen füge_Schwefel_hinzu ( ) und erhitze_Eisen_und_Schwefel ( ) wie folgt spezifizieren.

Allerdings reichen diese Axiome noch nicht aus, um

beweisen zu können, in der die in der Einleitung zu diesem Abschnitt beschriebene Aktionsreihenfolge zum Ausdruck kommt, wobei die Konstante die warte-Aktion repräsentiert. Insbesondere können wir noch nicht zeigen, daß in der durch beschriebenen Situation Eisen noch vorhanden ist, auch wenn es in der Situation ja vorhanden war. Formal bedeutet dies, daß keine logische Folgerung aus (4.12) und (4.13) ist.

Wir müssen also noch das in der Einleitung zu diesem Abschnitt besprochene Rahmenproblem lösen. Dies kann durch die Hinzunahme weiterer, sogenannter Rahmen- bzw. Kulissenaxiome geschehen, die festlegen, welche Fluenten bei Anwendung einer Aktion erhalten bleiben. Die nachfolgend aufgeführten Axiome sind davon diejenigen, die wir im Eisen und Schwefel Beispiel benötigen.

Wir können jetzt die Allgemeingültigkeit von

nachweisen, indem wir zB. die Formel in Matrixform überführen und die Konnektionsmethode anwenden. Abbildung 4.18 zeigt einen solchen Konnektionsbeweis.


Abbildung 4.18: Ein Konnektionsbeweis für (4.17).

In der hier dargestellten Form werden Kulissenaxiome benötigt, wobei die Anzahl der Fluenten und die Anzahl der Aktionen ist. Diese Anzahl läßt sich zwar durch eine geschicktere Repräsentation von Aktionen und Situation verringern (siehe zB. [Kow79]), trotzdem führt die Verwendung von Kulissenaxiomen zu einer Reihe von irrelevanten Ableitungen bei der Beweissuche. Die Lösungen für das Rahmenproblem im (monotonen) Situationskalkül waren so unbefriedigend, daß McCarthy vorschlug, nichtmonotone Inferenzregeln wie zB. die Zirkumskription (siehe Abschnitt 3.5) zu verwenden. Aber auch in einer nichtmonotonen Logik müssen Axiome zur Lösung des Rahmenproblems angegeben werden (siehe zB. [Rei92, Lif90a]). Beispielhaft sei hier nur das sogenannte Trägheitsgesetz (engl. law of inertia) genannt.

Abnormal ist das schon aus Kapitel 3 bekannte Prädikatszeichen, mit dem hier ausgedrückt wird, daß, wenn die Ausführung der Aktion in Situation das Fluent normalerweise nicht beeinflußt, dann der Wert von in der Situation gleich dem Wert von in ist.gif Wir wollen hier diesem Weg nicht weiter folgen, sondern überlegen, wie in einem monotonen logischen Kalkül erster Stufe Aktionen und Situationen dargestellt werden können, ohne daß für die Lösung des Rahmenproblems explizit Rahmenaxiome angegeben werden müssen.

Bevor wir uns jedoch dieser Fragestellung zuwenden, wollen wir noch einige abschließende Bemerkungen zum Situationskalkül machen. Der Situationskalkül ist im strengen Sinne eigentlich gar kein Kalkül, sondern beschreibt eine Methode, wie Situationen und Aktionen in der Sprache der (uU. nichtmonotonen) Prädikatenlogik formalisiert werden können. Diese Methode ist durchaus flexibel und erlaubt die verschiedensten Fragestellungen aus dem Bereich des Planens -- zB. Fragen nach der Dauer von Aktionen oder der parallelen Ausführbarkeit von Aktionen -- durch geschickte Wahl der Axiome zu modellieren und zu lösen. Der in [GLR91] gegebene Überblick zeigt die Stärken und Grenzen des Situationskalküls an vielen Beispielen auf.

Kommen wir nun zurück zum Planen und der Frage nach einer Lösung des Rahmenproblems. Die Arbeiten an diesem Problem haben sich in der Vergangenheit sehr stark an den Methoden des Situationskalküls orientiert. Diese einseitige Ausrichtung führte sogar zu dem Glauben, daß ohne explizite Angabe von Rahmenaxiomen das Rahmenproblem nicht gelöst werden kann (siehe zB. [Hay73b, HM87]). Wie wir in den nachfolgenden Abschnitten darlegen werden, gilt dies jedoch nicht. Schon McCarthy und Hayes wiesen in [MH69] einen Weg zur Lösung der Rahmenproblematik. Sie schlugen vor, einen Rahmen (oder eine Kulisse) zu verwenden, so wie beispielsweise ein Zustandsvektor in [McC62] benutzt wird, um eine Semantik für die Programmiersprache Algol angeben zu könnengif. Die Idee dabei ist, daß die Fluenten an dem Rahmen bzw. der Kulisse festgemacht sind. Die Vor- und Nachbedingungen von Aktionen legen genau fest, welche dieser Fluenten durch die Aktionen verändert werden. Alle übrigen Fluenten, die an dem Rahmen befestigt sind, bleiben unverändert.

Wir wollen im weiteren Verlauf des Kapitels drei Logiken angeben, die unabhängig voneinander entwickelt wurden und jeweils das Rahmenproblem ohne Angabe von Rahmenaxiomen lösen. Es sind dies die lineare Konnektionsmethode, eine um eine Gleichungstheorie erweiterte Hornlogik sowie die lineare Logik. Sodann werden wir aufzeigen, daß diese Logiken für eine große Klasse von Problemen äquivalent sind.



gif gif up gif contents index

Christoph Quix, Thomas List, René Soiron
30. September 1996