Information Technology Reference
In-Depth Information
Theorem 3.6.1.
Let
(
O; D
)
be a qualication scenario with transition model
and Fluent Calculus axiomatization FC
D
. Then for each model of
FC
D
[f
(3.7),(3.8),(2.37){(2.40)
g there exists a corresponding interpreta-
tion
(
Res ;
)
for
(
O; D
)
and vice versa.
Proof.
We conne ourselves to the dierences to the proof of Theorem 2.9.2,
which arise from the rened notion of qualied action sequences. The modi-
ed axiom (3.8) additionally requires that the fluent
disq
(
a
) be false in the
state resulting from performing
a
. This is exactly what distinguishes De-
nition 3.3.1 from Denition 2.7.2, regarding the notion of transition models.
Qed.
From now onwards, let|given a qualication scenario (
O; D
)|
W
(
O;D
)
denote the classical formulas
FC
D
[f
(3.7),(3.8),(2.37){(2.40)
g
plus the ax-
iomatization of the observations in
O
.
9
Observations
F
after [
a
1
;:::;a
n
] are
formalized as before, that is,
9s
[
Result
([
a
1
;:::;a
n
]
;s
)
^ Holds
(
F; s
) ]
(3.10)
while a disqualication observation
a
inexecutable after [
a
1
;:::;a
n
] is rep-
resented by
Qualied
([
a
1
;:::;a
n
])
^:Qualied
([
a
1
;:::;a
n
;a
])
(3.11)
As one would expect, there is a one-to-one correspondence between the set
of classical models of
W
(
O;D
)
and the set of models of the scenario (
O; D
).
Corollary 3.6.1.
Let
(
O; D
)
be a qualication scenario with axiomatiza-
tion W
(
O;D
)
, then for each model of W
(
O;D
)
there exists a corresponding
model
(
Res ;
)
of
(
O; D
)
and vice versa.
Proof.
Following Theorem 3.6.1 it suces to show that an observation is true
in
Res
i
is model of the observation's axiomatization.
1. By denition, an observation
F
after [
a
1
;:::;a
n
] is true in
Res
i
Res
([
a
1
;:::;a
n
]) is dened and formula
F
holds in that state. This
in turn is equivalent to
being a model of formula (3.10) according to
axiom (2.38), which stipulates that
9s: Result
(
a
;s
)i
Qualied
(
a
);
Proposition 2.9.3, which asserts that
Holds
is suitably dened; and the
fact that
and (
;Res
) correspond.
2. By denition, an observation
a
inexecutable after [
a
1
;:::;a
n
] is true
in
Res
i
Res
([
a
1
;:::;a
n
]) is dened but
Res
([
a
1
;:::;a
n
;a
]) is not.
This in turn is equivalent to
being a model of formula (3.11) according
to the fact that
and (
;Res
) correspond.
Qed.
9
The reason for the at rst glance unmotivated use of the letter
W
reveals in
the following section.
