Information Technology Reference
In-Depth Information
The core of this extension consists of two predicates
Qualied
(
a
) and
Result
(
a
;s
) with the following intuitive meaning. A valid instance of the
former indicates that the action sequence
a
is executable starting in the
initial state. A valid instance of the latter indicates that
s
represents the state
which would result from performing
a
in the initial state. As a notational
convention, if
a
is a (possibly empty) action sequence and
a
an action,
then [
a
ja
] shall denote the action sequence which consists in
a
followed
by
a
. The crucial, domain-independent properties of the new predicates are
determined by the following axioms:
Qualied
([ ])
(2.35)
Qualied
([
a
ja
])
Qualied
(
a
)
^9s; s
0
Result
(
a
;s
)
^
Successor
(
s; a; s
0
)
(2.36)
Result
([
a
ja
]
;s
0
)
8s
[
Result
(
a
;s
)
Successor
(
s; a; s
0
)] (2.37)
The reading of the topmost atomic formula, (2.35), is obvious. Formula (2.36)
states, in words, that an action sequence [
a
ja
] is qualied if so is
a
and
if there exists a successor
s
0
of
s
and
a
. Finally, implication (2.37) ensures
that
s
0
can only be the result of performing the sequence [
a
ja
] f
s
0
is
a possible successor when executing
a
in the state resulting from perform-
ing
a
. Notice, however, that the axioms (2.36) and (2.37) do not entail the
existence of a resulting state whenever the corresponding action sequence is
qualied, nor do they entail uniqueness of resulting states. We therefore need
to add the following:
9s: Result
(
a
;s
)
Qualied
(
a
)
(2.38)
Result
(
a
;s
)
^ Result
(
a
;s
0
)
s
=
s
0
(2.39)
Finally, the term intended to represent the initial state should qualify as
such, namely, both in being a proper state term and in satisfying all state
constraints, that is,
Result
([ ]
;s
)
State
(
s
)
^ Acceptable
(
s
)
(2.40)
In what follows, we prove that by introducing these domain-independent
axioms we achieve what we have promised. Suppose given a ramication
scenario (
O; D
) with transition model
, and let
FC
D
denote the encoding
of domain
D
as described in the previous section. Let
be some classical
interpretation of the set of formulas
FC
D
[f
(2.35){(2.40)
g
, and let (
;Res
)
be an interpretation for (
O; D
). Then we say that
and (
;Res
)
correspond
i for all action sequences
a
, states
S
, and collections of fluent literals
s
such that
EUNA j
=
s
=
S
we nd that
20
20
Below, by \ [
P
(
t
1
;:::;t
n
)]
is true" we mean that the
n
-tuple (
t
1
;:::;t
n
)is
member of the relation which interpretation
assigns to predicate
P
, where
t
i
(1
i n
) denotes the element of
's universe to which
maps term
t
i
.
