Information Technology Reference
In-Depth Information
Res
(
a
)=
S
i [
Result
(
a
;s
)]
is true
(2.41)
The notion of correspondence provides the basis for the correctness result of
the entire axiomatization.
Theorem 2.9.2.
Let
(
O; D
)
be a ramication scenario with transition model
, and let FC
D
be the axiomatization of D. Then for each model of
FC
D
[f
(2.35){(2.40)
g there exists a corresponding interpretation
(
;Res
)
for
(
O; D
)
and vice versa.
Proof.
\
)
":
Let
be a model of
FC
D
[f
(2.35){(2.40)
g
. We dene a partial mapping
Res
from nite action sequences to states as follows:
Res
(
a
) is dened when-
ever [
Qualied
(
a
)]
is true; and in case it is dened, let
s
be a collection
of fluent literals such that [
Result
(
a
;s
)]
is true, then
Res
(
a
)=
S
for
some
S
such that
EUNA j
=
s
=
S
. By induction on
n
, we prove that,
for any action sequence
a
=[
a
1
;:::;a
n
],
Res
(
a
) satises the condition of
constituting an interpretation. By construction, the interpretation (
;Res
)
then corresponds to
.
In the base case,
n
= 0, we have to show that
Res
([ ]) is dened and
satises the state constraints. According to axiom (2.35), [
Qualied
([ ])]
is true; hence,
Res
([ ]) is dened. Given that [
Qualied
([ ])]
is true, ax-
ioms (2.38) and (2.39) imply that there is a unique (modulo AC1N) term
s
such that [
Result
([ ]
;s
)]
is true. In conjunction with Proposition 2.9.2, for-
mula (2.40) guarantees that
s
represents a state, which, moreover, satises
the state constraints according to Proposition 2.9.3.
For the induction step let
n>
0 and suppose the claim holds for action
sequence [
a
1
;:::;a
n−
1
]. Let
a
=[
a
1
;:::;a
n−
1
]. We have to show that
a)
Res
([
a
ja
n
]) is dened i so is
Res
(
a
) and
(
Res
(
a
)
;a
n
) is not empty,
and
b)
Res
([
a
ja
n
])
2
(
Res
(
a
)
;a
n
).
From axiom (2.36) and the induction hypothesis for
a
we conclude that
[
Qualied
([
a
ja
n
])]
is true i
Res
(
a
) is dened and there exists a term
s
0
such that [
Successor
(
Res
(
a
)
;a
n
;s
0
)]
is true. This proves clause a) accord-
ing to Theorem 2.9.1. Moreover, axioms (2.38) and (2.39) imply that if
Res
([
a
ja
n
]) is dened, then there is a unique (modulo AC1N) term
s
such
that [
Result
([
a
ja
n
]
;s
)]
is true. From axiom (2.37), the induction hypothe-
sis for
a
, and Theorem 2.9.1 it follows that
s
represents a successor state
of
Res
(
a
) and
a
n
. This proves clause b).
\
(
":
Let (
;Res
) be an interpretation for (
O; D
), and let
be an interpretation
of
FC
D
[f
(2.35){(2.40)
g
which satises the following:
1.
is a model of
FC
D
.
