Database Reference
In-Depth Information
Fur den Beweis der Gegenrichtung sei nun umgekehrt
S
eine stabile Extension
von AS SMP .Da
S
konfliktfrei ist, kann es zu jedem m
M nach Definition von
hochstens ein w
W mit (m, w )
W hochstens ein m
∈S
und zu jedem w
M
mit (m ,w)
∈S
geben. Damit definiert
S
partielle Funktionen
S : M
W
und
T : W
M
mit S(m)=w , falls (m, w )
, und T (w)=m , falls (m ,w)
∈S
∈S
.Dadie
Annahme, es gabe ein (m, w)
M
×
W ,sodassfur alle w
W und fur alle m
M
sowohl (m, w )
gilt, im Widerspruch zur Stabilitat von
S steht, ist S sogar eine totale, bijektive Abbildung und es gilt S −1 = T .Umzu
zeigen, dass S eine Losung des SMP ist, machen wir die Widerspruchsannahme,
dass es ein instabiles Paar gibt, d.h.
∈S
als auch (m ,w)
∈S
w S −1 (w).
(m, w)
M
×
W
mit w
m S(m) und m
und (S −1 (w),w)
Aus (m, S(m))
∈S
∈S
folgt (m, w) /
∈S
wegen der Konfliktfreiheit
von
S
.Da
S
eine stabile Extension ist, muss
S
(m, w) gelten. Die beiden einzig
moglichen Angriffe von
S
auf (m, w)sind(m, S(m))
(m, w) und (S −1 (w),w)
(m, w). Der erste Angriff steht aber im Widerspruch zu w
m S(m) und der zweite
m S −1 (w). Die Zuordnung S ist damit stabil und
Angriff im Widerspruch zu m
daher eine Losung des SMP.
Wenn man im SMP gleichgeschlechtliche Ehen zulasst, gibt es keine stabile
Extension im entsprechenden Argumentationssystem; eine Losung des stabilen Hei-
ratsproblems entspricht dann einer bevorzugten Extension (s. [57]).
10.3.4
Beziehungen zur Reiter'schen Default-Logik
Der Begriff der Extension als eine ausgezeichnete Menge von Objekten taucht auch
in den Default-Logiken (Kapitel 8) auf. Im Folgenden wollen wir zeigen, dass Exten-
sionen einer Reiter'schen Default-Theorie als Extensionen eines Argumentationssys-
tems aufgefasst werden konnen.
Sei T =(W, Δ) eine Reiter'sche Default-Theorie; wir nehmen außerdem im
Folgenden an, dass W konsistent ist. Fur Δ =
{
δ 1 ,...,δ n }
bezeichnet
Just (Δ) = just 1 )
...
just n )
die Menge aller Begrundungen, die in den Defaults aus Δ vorkommen (vgl. Defini-
tion 8.3).
Sei K
Just (Δ) eine Menge von Begrundungen. Eine (klassische) Formel F
heißt unsichere Konsequenz aus T und K, wenn es eine Folge L 0 ,L 1 ,...,L n von
Formeln mit L n = F gibt, so dass fur jedes L i eine der folgenden Aussagen zutrifft:
L i
W oder
L i
Cn (
{
L 0 ,L 1 ,...,L i−1 }
)oder
L i = cons (δ)mit pre (δ)
∈{
L 0 ,L 1 ,...,L i−1 }
und just (δ)
K.
Search WWH ::




Custom Search