Information Technology Reference
In-Depth Information
2. For any action sequence
a
and collection of fluent literals
s
,
a) [
Qualied
(
a
)]
is true if and only if
Res
(
a
) is dened, and
b) [
Result
(
a
;s
)]
is true if and only if both
Res
(
a
) is dened and
EUNA j
=
s
=
Res
(
a
)
.
We have to show that
is a model of
FC
D
[f
(2.35){(2.40)
g
, in which case it
corresponds to (
;Res
) by construction. Given that
is a model of
FC
D
,
it suces to show that it is also a model of axioms (2.35){(2.40). This in turn
can be proved by induction on the length of the argument
a
of
Qualied
and
Result
. This induction proof is completely analogous to the above.
Qed.
2.9.4 Encoding Observations
The theorem at the end of the previous section shows the adequacy of the
domain-independent axioms (2.35){(2.40) as regards the formal notion of
states resulting from performing action sequences. Next, and nally, we con-
centrate on the scenario-specic expressions that are based on this concept,
namely, the observations. Their axiomatization is straightforward. Any ob-
servation
F
after [
a
1
;:::;a
n
] is encoded by the formula
9s
[
Result
([
a
1
;:::;a
n
]
;s
)
^ Holds
(
F; s
) ]
(2.42)
That is to say, the action sequence [
a
1
;:::;a
n
] must admit a resulting state
in which, moreover, fluent formula
F
holds. The addition of these formulas
automatically restricts the set of classical models to those which correspond
to interpretations in which the respective observations are true. Let (
O; D
)
be a ramication scenario, then by
FC
(
O;D
)
we denote its axiomatization
FC
D
[f
(2.35){(2.40)
g[f
V
o2O
(2
:
42)
g
. Then classical entailment wrt. this
axiomatization and the notion of entailment in our action theory coincide.
Corollary 2.9.1.
Let
(
O; D
)
be a ramication scenario with axiomatiza-
tion FC
(
O;D
)
. An observation F
after [
a
1
;:::;a
n
]
is entailed by
(
O; D
)
i
FC
(
O;D
)
entails the formula 9s
[
Result
([
a
1
;:::;a
n
]
;s
)
^ Holds
(
F; s
)]
.
Proof.
Let
be a model of
FC
(
O;D
)
and (
;Res
) a corresponding inter-
pretation. Given Theorem 2.9.2, it suces to show that
is a model of
formula (2.42) i the corresponding observation is true in (
;Res
). By de-
nition,
F
after [
a
1
;:::;a
n
] is true in (
;Res
)i
Res
([
a
1
;:::;a
n
]) is dened
and
F
is true in that state. This in turn is equivalent to
being model of
9s
[
Result
([
a
1
;:::;a
n
]
;s
)
^ Holds
(
F; s
) ] according to axiom (2.38), Propo-
sition 2.9.3, and the fact that
and (
;Res
) correspond.
Qed.
Example 2.9.2.
Let
D
be the ramication domain modeling the electric cir-
cuit consisting of two switches and a light bulb of Fig. 2.3 as in Example 2.2.2.
Furthermore, let
FC
D
be its axiomatization as explicated at the end of Sec-
tion 2.9.2. Let
O
consist of the single observation
