Database Reference
In-Depth Information
11.4
Probleme
11.4.1
Das Rahmenproblem
Die am Ende des vorigen Abschnitts erlauterte Schwierigkeit, Gultigkeit von For-
meln auf nachfolgende Situationen zu ubertragen, ist als das sog.
Rahmenproblem
(
frame problem
) bekannt. Die Vorstellung dabei ist, dass sich alles, was sich ge-
wissermaßen als Rahmen um die betrachtete Operatoranwendung befindet, auf die
neue Situation ubertragt. Um zu formalisieren, dass sich zwei Blocke, die beide bei
einer
STACK
-Operation nicht bewegt wurden, noch aufeinander befinden, wenn dies
vorher der Fall war, benutzen wir folgende Formel:
∧
=
u
⇒
ON(x,y,s)
x
ON(x,y,do(STACK(u,v),s))
Umgekehrt mussen wir auch noch formalisieren, dass sich ein Block nach einer
STACK
-Operation nicht auf einem anderen befindet, wenn dies vorher nicht der Fall
war und er bei der Operation nicht darauf gesetzt wurde:
¬
ON(x,y,s)
∧ (
x
=
u
∨
y
=
v
) ⇒¬
ON(x,y,do(STACK(u,v),s))
Diese Art von Formeln werden
Rahmenaxiome
(
frame axioms
) genannt. In Analogie
zu positiven und negativen Effektaxiomen ist das zuerst angefuhrte Rahmenaxiom
ein
positives
, das zweite ein
negatives
Rahmenaxiom. Zu allem Uberfluss reichen aber
die beiden angegebenen Rahmenaxiome fur den
STACK
-Operator selbst in unserer
einfachen Blockwelt immer noch nicht aus. Neben dem Nicht-Effekt auf die Relation
ON
mussen wir auch noch Rahmenaxiome bzgl. der anderen relationalen Fluents
ONTABLE
und
CLEAR
angeben.
Ein Block befindet sich auch nach einer
STACK
-Operation auf dem Tisch bzw.
nicht auf dem Tisch, wenn er bei der Operation nicht bewegt wurde:
ONTABLE(x,s)
∧
x
=
u
⇒
ONTABLE(x,do(STACK(u,v),s))
¬
ONTABLE(x,s)
∧
x
=
u
⇒¬
ONTABLE(x,do(STACK(u,v),s))
Selbsttestaufgabe 11.3 (Rahmenaxiome)
Formulieren Sie zunachst verbal
und dann in Pradikatenlogik Rahmenaxiome fur den
STACK
-Operator bzgl. der Re-
lation
CLEAR
.
Auch fur den
UNSTACK
-Operator (vgl. Selbsttestaufgabe 11.1) mussen wir explizite
Rahmenaxiome angeben. Analog zur Situation bei
STACK
sind das jeweils Rah-
menaxiome fur die relationalen Fluents
ON
,
ONTABLE
und
CLEAR
:
ON(x,y,s)
∧
x
=
u
⇒
ON(x,y,do(UNSTACK(u,v),s))
¬
ON(x,y,s)
⇒¬
ON(x,y,do(UNSTACK(u,v),s))
⇒
ONTABLE(x,s)
ONTABLE(x,do(UNSTACK(u,v),s))
¬
ONTABLE(x,s)
∧
x
=
u
⇒¬
ONTABLE(x,do(UNSTACK(u,v),s))
⇒
CLEAR(x,s)
CLEAR(x,do(UNSTACK(u,v),s))
¬
CLEAR(x,s)
∧
x
=
v
⇒¬
CLEAR(x,do(UNSTACK(u,v),s))
