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.
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.
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 FormHierbei sind natürlich auch leere Konjunktionen zugelassen. Man beachte, daß ohne die genannte Richtung in einer solchen Regel das, wobei
eine Konjunktion von Atomen und
eine Konjunktion negierter Atome ist.
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ündungWie 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.stützt den Knoten
relativ zu einer Interpretation
, wenn
in
wahr ist.
Ein ModellDie Gerichtetheit der Regeln geht in diese Definition ganz wesentlich mit ein, wie das folgende Beispiel zeigt. Es seieneiner 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.
Zu einer MengeMit 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.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.
Ein Modell einer Menge von Begründungen ist stabil genau dann, wenn es fundiert ist.Man sieht leicht, daß die schon oben betrachtete Menge
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 NieteDie 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.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.
Eine Nietenstrategie , die[Elk90] gibt eine denkbar einfache Nietenstrategie an, die das folgende Lemma formuliert.und
auf
abbildet, heißt korrekt, wenn
- jedes Modell von
, das
falsifiziert, sich zu einem fundierten Modell von
erweitern läßt, und wenn
- jedes auf die in
auftretenden Knoten beschränkte fundierte Modell von
ein fundiertes Modell von
ist, das
falsifiziert.
SeienZur 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].und
neue Knoten bezüglich einer Begründungsmenge
. Dann ist die Nietenstrategie, die
und
auf
abbildet, korrekt.
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.
Christoph Quix, Thomas List, René Soiron