Database Reference
In-Depth Information
11.3.5
Zielbeschreibungen
Als Zielbeschreibungen lassen wir existentiell quantifizierte Konjunktionen wie
t ON(A,B,t) ON(B,C,t)
zu. Man beachte, dass eine solche Zielbeschreibung im Allgemeinen nicht eindeutig
ist. So wird im gegebenen Beispiel die Zielbeschreibung erfullt, wenn A auf B und B
auf C steht, unabhangig davon, wo C steht, ob noch ein weiterer Block auf A steht
oder wo sich eventuell noch zusatzliche Blocke befinden.
Gegeben sei der in Abbildung 11.1(a) skizzierte Zustand. Wenn nun eine von
S0 ausgehende, konstruktive Beschreibung von t gefunden wird, in der die obige
Zielbeschreibung gilt, so konnen wir daraus einen Plan erstellen, der den Ausgangs-
zustand in einen gewunschten Zielzustand uberfuhrt. Wenn wir im vorliegenden Fall
die Variablen x, y und s der im vorigen Abschnitt angegebenen Ausfuhrungsbe-
dingung fur STACK ersetzen durch A, B und S0 , so erhalten wir die Formel
Poss(STACK(A,B),S0) ONTABLE(A,S0)
CLEAR(A,S0)
CLEAR(B,S0)
die offensichtlich in S0 gilt. Damit ist die Instanz STACK(A,B) des STACK -Operators
in S0 anwendbar. Als Nachbedingungen fur die in Abschnitt 11.3.4 angegebenen
Effektaxiome fur STACK(A,B) erhalten wir
ON(A,B,do(STACK(A,B),S0))
¬ CLEAR(B,do(STACK(A,B),S0))
¬
ONTABLE(A,do(STACK(A,B),S0))
Damit haben wir eine Situation t = do(STACK(A,B),S0) gefunden, so dass
ON(A,B,t) gilt. Dabei ist t = do(STACK(A,B),S0) insofern eine konstruktive Be-
schreibung, als dass man daraus den Plan “Staple in der Situation S0 Block A auf
Block B ” direkt ablesen kann. Einsetzen von t in die ursprungliche Zielformel ergibt
ON(A,B,do(STACK(A,B),S0)) ON(B,C,do(STACK(A,B),S0))
Selbsttestaufgabe 11.2 (Situationskalkul) Ist mit den bisherigen Formalisie-
rungen sichergestellt, dass in der Situation t = do(STACK(A,B),S0) immer noch
Block B auf Block C liegt? Mit anderen Worten, kann mit dem bisher Gesagten die
Formel ON(B,C,do(STACK(A,B),S0)) abgeleitet werden?
Auf der einen Seite ist zu beachten, dass sich eine Operatoranwendung im
Situationskalkul nur auf die Formeln der Nachfolgesituation auswirkt, aber nicht
auf die der Ausgangssituation. Wenn in Situation S0 Block A auf B gesetzt wur-
de, so gilt immer noch, dass sich A in S0 auf dem Tisch befand; die Formel
ONTABLE(A,S0) ist immer noch wahr und steht auch nicht im Widerspruch zu
der Formel ON(A,B,do(STACK(A,B),S0)) , die ebenfalls wahr ist. Auf der ande-
ren Seite ubertragt sich die Gultigkeit einer Formel in einer Situation nicht ohne
weiteres auf eine Nachfolgesituation: Aus ON(B,C,S0) konnen wir (bisher) nicht
ON(B,C,do(STACK(A,B),S0)) schließen.
Search WWH ::




Custom Search