5
similarly
?
F
(
~x; a; s
) describ es the conditions under which performing
a
in
s
results
in
F
becoming false in the successor situation. The solution to the frame problem
of [23] rests on a
completeness assumption
, which is that the causal axioms (2.6)
and (2.7) characterize all the conditions under which action
a
can lead to a uent
F
(
~x
) b ecoming true (respectively, false) in the successor situation. In other words,
axioms (2.6) and (2.7) describ e all the causal laws aecting the truth values of the
uent
F
. Therefore, if action
a
is p ossible and
F
(
~x
)'s truth value changes from
false
to
true
as a result of doing
a
, then
+
F
(
~x; a; s
) must be
true
and similarly for a
change from
true
to
false
. Reiter [23] shows how to derive a
successor state axiom
of the following form from the causal axioms (2.6) and (2.7) and the completeness
assumption.
Successor State Axiom
P oss
(
a; s
)
[
F
(
~x; do
(
a; s
))
+
F
(
~x; a; s
)
_
(
F
(
~x; s
)
^ :
?
F
(
~x; a; s
))]
This single axiom embodies a solution to the frame problem. Notice that this axiom
universally quanties over actions
a
. In fact, this is one way in which a parsimonious
solution to the frame problem is obtained.
Applying this to our example ab out breaking things, we obtain the following
successor state axiom:
P oss
(
a; s
)
[
brok en
(
x; do
(
a; s
))
(
9
r
)
f
a
=
drop
(
r; x
)
^
f rag ile
(
x; s
)
g _
(
9
b
)
f
a
=
explode
(
b
)
^
nexto
(
b; x; s
)
g _
brok en
(
x; s
)
^ :
(
9
r
)
a
=
repair
(
r; x
)]
:
It is imp ortant to note that the above solution to the frame problem presupp oses
that there are no
state constraints
, as for example in the blocks world constraint:
(
8
s
)
:on
(
x; y ; s
)
:
on
(
y; x; s
). Such constraints sometimes implicitly contain eect
axioms (so-called indirect eects), in which case the above completeness assump-
tion will not b e true. The assumption that there are no state constraints in the
axiomatization of the domain will be made throughout this pap er. In [17, 15], the
approach discussed in this section is extended to deal with state constraints, by
compiling their eects into the successor state axioms.
2.5. Axiomatizing an Application Domain in the Situation Calculus
In general, a particular domain of application will b e sp ecied by the union of the
following sets of axioms:
Action precondition axioms, one for each primitive action.
Successor state axioms, one for each uent.
Unique names axioms for the primitive actions.
Axioms describing the initial situation { what is true initially, b efore any
actions have o ccurred. This is any nite set of sentences which mention no
situation term, or only the situation term
S
0
.
Foundational, domain indep endent axioms for the situation calculus. These
include unique names axioms for situations, and an induction axiom. Since
these play no sp ecial role in this paper, we omit them. For details, and for
their metamathematical properties, see Lin and Reiter [17] and Reiter [24].