Database Reference
In-Depth Information
J
J
6
}
J
6
fundiert gultig
SJ(F )=J
6
Supp(F )=
(F )=
{
{
C, E
}
Label
(F )=
in
Cons(F )=
∅
Mittlerweile sind die Label von A, B, C, D, F bekannt.
Das neue Modell ist M
=
(6)
{
A, C, D, E, F
}
.
Widerspruchsknoten existieren nicht.
(7)
Die Knoten A, B, C, F haben ihren Status gewechselt.
Nun erklaren sich auch die Bezeichnungen
monotone
und
nichtmonotone
Be-
grundung (vgl. Definition 7.3): Ist die stutzende Begrundung eines Knotens eine
monotone Begrundung (d.h. besitzt eine leere
out
-Liste), so wird der Knoten bei
Hinzunahme faktischer Information (Pramissen) seinen Status nicht andern, so lan-
ge auch die
in
-Knoten seiner stutzenden Begrundung ihren Status beibehalten.
Anders verhalt es sich, wenn die stutzende Begrundung nichtmonoton ist, also eine
nichtleere
out
-Liste hat. In diesem Fall kann - auch bei gleichbleibendem Status
der
in
-Knoten - durch den Statuswechsel eines
out
-Knotens auch der Knoten selbst
seinen Status andern.
Knoten, deren stutzende Begrundungen nichtmonotoner Natur sind, haben al-
so einen weniger soliden Status und werden demzufolge manchmal auch als die
Annahmen
eines Modells bezeichnet. In Beispiel 7.4 ist der Knoten B die einzige
Annahme.
Kommen wir nun zur Vorstellung des DDB-Algorithmus. Er wird, wie bereits
gesagt, gestartet, wenn das System feststellt, dass ein Widerspruchsknoten n
⊥
in
ist. In diesem Verfahren wird die Menge MaxAnn(n
⊥
)der
maximalen Annahmen
des Widerspruchsknotens benotigt. Dazu bestimmt man zunachst einmal die Fun-
damente Ant
∗
(n
⊥
) des Widerspruchsknotens, also den transitiven Abschluss der
Antezedenzen von n
⊥
, und betrachtet dort nur die Annahmen. Eine Annahme n
A
ist genau dann in MaxAnn(n
⊥
) enthalten, wenn n
A
∈
Ant
∗
(n
⊥
) ist und es keine
andere Annahme n
B
∈
Ant
∗
(n
⊥
)gibtderart,dassn
A
∈
Ant
∗
(n
B
)ist.Weiterhin
sei
J
⊥
die Menge der stutzenden Begrundungen der Knoten in MaxAnn(n
⊥
).
Prozedur Dependency Directed Backtracking - DDB
Eingabe:
Ein TM-Netzwerk;
ein zulassiges Modell M ;
ein Widerspruchsknoten n
⊥
mit Status
in
.
Ausgabe:
Ein zulassiges Modell bzgl. eines erweiterten TM-Netzwerks oder Mel-
dung eines unlosbaren Widerspruchs.
2
1. Bestimme die Menge MaxAnn(n
⊥
) der maximalen Annahmen von n
⊥
.Ist
MaxAnn(n
⊥
)=
∅
, so liegt ein unlosbarer Widerspruch vor; HALT.
2
Da dieser Algorithmus den JTMS-Algorithmus verwendet, gelten auch hier die Einschrankungen
bzgl.
odd loops
(vgl. Seite 219).
