Nach diesen theoretischen Vorbereitungen kommen wir nun zurück zu unserer eigentlichen Fragestellung eines Begründungsverwaltungssystems. Im folgenden werden wir nun zwei solcher Systeme kurz besprechen. Sie unterscheiden sich in den folgenden drei wesentlichen Merkmalen. Das erste Merkmal eines BVS ist die durch das System realisierte Logik. Das zweite Merkmal ist die bei der Repräsentiation der Information verwendete Datenstruktur. Schließlich geht es auch jeweils um eine spezielle Strategie.
Das erste hier zu besprechende System wurde unter dem Akronym ATMS (engl.
assumption-based truth maintenance system) bekannt [dK86]. Es stellt
einen eingeschränkten Spezialfall des vorweg besprochenen allgemeinen
Klauselverwaltungssystems insofern dar, als es nur Hornklauseln zuläßt,
im übrigen jedoch klassische Aussagenlogik realisiert. Die Idee eines
solchen annahmebasierten
Begründungsverwaltungssystems
ist, für jede
aussagenlogische Variable , (ob Annahme oder nicht), etwa einer Anfrage
im Sinne des eingangs erläuterten Beispiels, eine minimale Begründung,
dh. eine minimale Stützklausel auf der Basis des jeweiligen
, zu
berechnen und in die Datenstruktur mit aufzunehmen, genauso wie es in den
beiden Matrizen am Ende der Einleitung zu diesem Abschnitt illustriert wurde.
Dies ermöglicht eine explizite Darstellung der Abhängigkeit einer solchen
Aussage von den getroffenen Annahmen und erleichtert so die Modifikation im
Falle von Revisionen der Annahmemenge in der gewünschten Weise. Was wir dort
im Rahmen der Matrixdarstellung durch den einfachen Mechanismus der
Indizierung realisiert haben, wird hier durch eine Menge von
Knoten
realisiert, die die folgende Struktur
aufweisen.
De Kleer nannte diese Menge eine widerspruchsfreie,
konsistente,
vollständige und minimale Markierung für . Aus ihr sind
widersprüchliche Stützklauseln, sogenannte ``Nieten'' (engl.
nogoods), bereits
eliminiert (werden aber im System gesondert mitgespeichert). Nach der obigen Folgerung sind die Kontexte wie folgt durch Primimplikanten charakterisiert.
Die Menge der Kontexte wächst exponentiell mit der Zahl der Annahmen, so daß die Berechnung bald an Grenzen stößt. Verfahren zur Berechnung von Markierungen auf dem Wege über Primimplikanten wurden in [JP90] auf der Grundlage der Konnektionsmethode in der oben illustrierten Weise entwickelt. Hat man die Markierungen, so beschleunigen sich die in verschiedenen Kontexten erforderlichen Berechnungen jedoch in signifikanter Weise, was zB. auch für das Problem der Erfüllung von Randbedingungen [Bib88b] (engl. constraint satisfaction) von Bedeutung ist.
Wie die oben besprochenen allgemeineren Klauselverwaltungssysteme zeigen, kann ein ATMS ohne weiteres in zweifacher Weise verallgemeinert werden. Zum einen können auch Nicht-Hornklauseln, zum anderen Anfragen in Form von Klauseln statt nur Aussagenvariablen zugelassen werden.
Christoph Quix, Thomas List, René Soiron