Nächste Seite: 3.11 Vergleichende Zusammenfassung Vorige Seite: 3.10.2 ATMS

3.10.3 TMS

Die zweite Gattung von Begründungsverwaltungssystemen, die wir hier nennen, ist TMS [Doy79, McA80] (engl. truth maintenance system). Das Vorgehen ist durch das alltägliche Schließen basierend auf Annahmen inspiriert. Es sind daher Einflüsse von Gentzens Kalkül des natürlichen Schließens [Gen35] unverkennbar. Wie bei ATMS (das sich aus TMS entwickelt hat) werden auch hier Knoten mit einer Struktur verwandt, die der oben angegebenen ähnlich ist, jedoch mit den beiden folgenden Unterschieden. Erstens geht es nicht um die Kodierung des gesamten zu einem Knoten gehörenden Abhängigkeitsgeflechtes; die Markierung der oben beschriebenen Art entfällt daher. Zweitens werden de facto Ermangelungsregeln (statt Hornregeln) in Betracht gezogen, wie sie im Abschnitt 3.7 beschrieben sind. Dies tritt in TMS in Gestalt der ``outlist'' in Erscheinung, einer Liste von Prämissen, von denen zur Folgerung auf die Aussage des Knotens vorausgesetzt wird, daß sie nicht gelten. Die Negationen dieser Prämissen stellen im Sinne der Ermangelungsregeln die Rechtfertigungen dar, deren Konsistenz gewährleistet sein muß. Kurz, die Struktur eines Knotens ist hier die folgende.

: ; inlist, outlist>

Die Elemente der ``inlist'' entsprechen den Begründungen von ATMS. Wir haben uns dabei nicht an die Originalsyntax gehalten, sondern uns an die bereits oben eingeführte Form angelehnt. Der deduktive Zusammenhang, der durch eine solche Menge von Knoten repräsentiert wird, läßt sich anschaulich durch ein Abhängigkeitsnetz [Goo87] darstellen, wie es für den Fall des folgenden Beispiels in Abbildung 3.6 gezeigt ist.

Abbildung 3.6: Ein Abhängigkeitsnetz

Das Beispiel bezieht sich auf die Einrichtung eines Zimmers. Seine Faktenmenge besteht aus {Schreibtisch, vor_Fenster Blick_auf_Fenster}. Weiter enthält es die folgenden beiden Ermangelungsregeln.

Die Regeln sind in der Abbildung als Schaltungen mit Prämissen und einer Konklusion dargestellt, deren Bedeutung selbsterklärend ist. Der Bezug mit der TMS Darstellung ist der folgende. Die Konklusion ist der Wert des zugehörigen Knotens, dh. das in . Auf die in der Schaltung mit ``Out'' markierten Prämissen wird in der Knotendarstellung durch das Auftreten ihres Knotennamens in der ``outlist'' verwiesen, während das Gleiche für die mit ``In'' markierten Aussagen bezüglich der ``inlist'' gilt. In dem Beispiel ergibt sich als Lösung die Aufstellung des Schreibtisches mit Blick auf das Fenster als einzige Lösung.

Damit haben wir die einem TMS zugrundeliegende Datenstruktur beschrieben, seine Logik aber nur vage angedeutet. Letzteres soll nun präzisiert werden [Elk90].

Eine (TMS-) Begründung (engl. justification) ist eine gerichtete aussagenlogische Regel der Form , wobei eine Konjunktion von Atomen und eine Konjunktion negierter Atome ist.

Hierbei sind natürlich auch leere Konjunktionen zugelassen. Man beachte, daß ohne die genannte Richtung in einer solchen Regel das mit jedem Atom in vertauscht werden könnte. Genau eine solche Vertauschung ist aber durch die Richtung ausgeschlossen.

Wie in der Einleitung erläutert, besteht eine der Aufgaben eines BVS darin, eine Menge von Annahmen abduktiv zu erschließen, aus denen sich die gestellten Anfragen widerspruchsfrei ableiten lassen. Da in der Aussagenlogik jede Menge von Atomen (also auch der genannten Annahmen) eine Interpretation darstellt, läßt sich diese Aufgabe daher auch als die nach der Suche einer solchen Interpretation auffassen, die gewisse Eigenschaften hat. Eine dieser Eigenschaften muß sein, daß das Wahrsein unter der Interpretation von den Prämissen zur Konklusion der gerichteten Regeln weitergereicht wird, was in der folgenden Definition ausgedrückt wird.

Eine Begründung stützt den Knoten relativ zu einer Interpretation , wenn in wahr ist.

Wie in der Ermangelungslogik läuft man aber mit Regeln, die negative Prämissen enthalten, in die Gefahr einer zirkulären Schlußkette, die durch die folgende Definition ausgeschaltet wird.

Ein Modell einer Menge von Begründungen heißt fundiert, wenn es zu jedem mindestens eine Begründung gibt, die stützt und deren Atome in eine Teilmenge von bilden.

Die Gerichtetheit der Regeln geht in diese Definition ganz wesentlich mit ein, wie das folgende Beispiel zeigt. Es seien und . Klassisch sind beide äquivalent mit ; dennoch haben sie verschiedene fundierte Modelle (und zwar je genau eines), nämlich im Falle von und im Falle von . Das einzige fundierte Modell der Menge ist . Es ist leicht nachzuprüfen, daß in dieser alphabetischen Reihenfolge die erforderlichen Bedingungen erfüllt sind. Aus dem nachfolgenden Satz folgt außerdem, daß es kein weiteres Modell mehr gibt. Für diesen Satz benötigen wir noch die folgenden Begriffe [GL88].

Zu einer Menge von Begründungen und einer Interpretation sei die Menge derjenigen Begründungen, die man aus erhält durch (i) Streichung aller Begründungen mit einer negativen Prämisse , wenn in wahr ist, und (ii) Entfernung aller negativen Prämissen in allen verbleibenden Regeln.

Weiter heißt ein Modell von inklusionsminimal , wenn es keine echte Teilmenge gibt, die Modell von ist.

Schließlich heißt eine stabile Menge von , wenn sie ein inklusionsminimales Modell von ist.

Mit diesen Begriffen sind wir unversehens in die Semantik der in Abschnitt 3.4 bereits besprochenen Logikprogramme geraten. Auch Logikprogramme bestehen aus gerichteten Regeln der durch die TMS-Begründungen gegebenen Form. Wie wir aus Abschnitt 3.4 wissen, ist in ihnen die Negation zugelassen, wird aber nicht als klassische Negation interpretiert. Vielmehr sprechen wir von der Negation als Mißerfolg (engl. negation as failure), wobei der Mißerfolg eines Versuches gemeint ist, die unnegierte Aussage zu beweisen. Offensichtlich sind daher Logikprogramme auch nichtmonoton, denn durch die Hinzunahme neuer Aussagen kann ein solcher Mißerfolg ja aufgehoben werden. Stabile Mengen bilden also eine Semantik für Logikprogramme. Hier sind wir nun insbesondere an der Beziehung mit den TMS-Begründungen interessiert.

Ein Modell einer Menge von Begründungen ist stabil genau dann, wenn es fundiert ist.

Man sieht leicht, daß die schon oben betrachtete Menge ein zweites inklusionsminimales Modell, nämlich , besitzt. Allerdings ist es nicht stabil und folglich auch nicht fundiert.

Die soeben dargestellte Sicht von TMS-Begründungen als Logikprogramme ist nicht die einzig mögliche. Liest man nämlich jede negative Prämisse einer Begründung als , so erhält man eine ähnliche Charakterisierung mittels der autoepistemischen Logik , was wir im einzelnen hier nicht mehr durchführen wollen [Elk90]. Man beachte jedoch, daß diese Charakterisierungen die Logikprogrammierung als gleichwertig mit TMS ebenso wie mit der autoepistemischen Logik, und umgekehrt, erweisen.

Bis hierher haben wir das Augenmerk auf die Logik und die Datenstruktur der BVS gerichtet und den algorithmischen Aspekt außer acht gelassen. Um dies nachzuholen, erinnern wir noch einmal an das in Abschnitt 3.10.1 angegebene Modell, bestehend aus den zwei Komponenten Problemlöser und Klauselverwaltungssystem. Aus verschiedenen Gründen kann der Problemlöser eine vom Klauselverwalter erarbeitete Annahmemenge (bzw. ein fundiertes Modell) als untauglich erklären. Der häufigste Grund ist eine sich ergebende Widersprüchlichkeit. Wir sprechen dann von einer Niete (engl. nogood). Ist eine solche Niete, so heißt dies, daß alle akzeptablen Modelle auch wahr machen müssen, da alle getroffenen Annahmen in ihnen wahr sein müssen. Durch Einführung eines neuen Atoms als Niete und der Begründung können wir immer Nieten als Atome annehmen, weil dann offensichtlich die zusätzliche Begründung äquivalent mit ist. Um Nieten auszuschalten, müssen die Begründungen abgeändert werden, die zu ihnen führten. Diese Idee erfaßt die folgende Definition.

Eine Nietenstrategie ist ein Algorithmus, der zu einer Niete und einer Begründungsmenge als Eingabe eine Begründungsmenge mit möglicherweise neuen Knoten so erzeugt, daß kein fundiertes Modell von die Niete erfüllt.

Die in diesem Gebiet bekanntgewordenen abhängigkeitsgesteuerten Rücksetzalgorithmen (engl. dependency-directed backtracking) [CRM80, Doy79] stellen Nietenstrategien dar. Sie verfolgen all die Begründungen rückwärts, die zu der Niete geführt haben, und ändern durch Hinzunahme einer neuen Begründung den Wahrheitswert einer der Ausgangsaussagen so ab, daß sich die Niete nicht mehr herleiten läßt. Diese theoretisch nicht umfassend durchdachten Verfahren weisen aber Mängel auf, die von dem folgenden Vorgehen vermieden werden.

Eine Nietenstrategie , die und auf abbildet, heißt korrekt, wenn

1. jedes Modell von , das falsifiziert, sich zu einem fundierten Modell von erweitern läßt, und wenn
2. jedes auf die in auftretenden Knoten beschränkte fundierte Modell von ein fundiertes Modell von ist, das falsifiziert.

[Elk90] gibt eine denkbar einfache Nietenstrategie an, die das folgende Lemma formuliert.

Seien und neue Knoten bezüglich einer Begründungsmenge . Dann ist die Nietenstrategie, die und auf abbildet, korrekt.

Zur Ausschaltung einer Niete braucht man also nur drei Begründungen dieser Gestalt hinzuzufügen, so daß sich ein Rücksetzverfahren zu diesem Zweck völlig erübrigt. Es kann allerdings zur Bestimmung der fundierten Menge nützlich sein. Diese Bestimmung kann sehr aufwendig sein, da sie ein NP-vollständiges Problem darstellt [Elk90].

Im übrigen wollen wir hinsichtlich der weiteren algorithmischen Behandlung eines TMS wegen des illustrierten Zusammenhanges mit den Ermangelungssystemen auf die Ergebnisse des letzten Abschnittes verwiesen werden. Eines der Verfahren wird in [JK90] vorgestellt. Auf ihm basiert ein an der GMD, St. Augustin, entwickeltes System, EXCEPT, das eine Ermangelungslogik mit Hilfe eines TMS realisiert. Weitere Details zu dem gesamten Komplex der Begründungsverwaltungssysteme findet man in [Sto88].

In [McD91] wird eine alternative Formalisierung von Begründungsverwaltungssystemen beschrieben, die hinsichtlich der möglichen deduktiven Folgerungen eingeschränkter ist und daher auch effizienter zu sein scheint.