Nächste Seite: 3.10.3 TMS Vorige Seite: 3.10.1 Klauselverwaltungssysteme

3.10.2 ATMS

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.

: ; Markierung; Begründungen >

ist die genannte Aussage, deren Abhängigkeit von den Annahmen durch den Knoten charakterisiert werden soll. Als (ATMS-) Begründungen werden alle Regeln in bezeichnet, deren Konklusion ist. Durch sie wird eine Vorgängerstruktur auf der Knotenmenge implizit festgelegt. Praktisch genügt es, für jede Regel die Liste seiner Prämissen hier anzugeben. Eine Markierung (unser Index bzw. in den oben dargestellten Matrizen) ist eine Menge von Kontexten, wobei diese Menge gegeben ist durch

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.