Information Technology Reference
In-Depth Information
Proof.
1. We rst prove
Ψ
S
i
=0
Ψ
i
and
^
S
i
=0
i
.
a) Let
F 2 Ψ
. Then minimality of (
Ψ;
^
) implies the existence of
a nite sequence
"
1
causes
%
1
if
1
;:::;"
n
causes
%
n
if
n
of
causal relationships in
R
such that
F 2Th
(
Ψ [f%
1
;:::;%
n
g
)
and, for each 1
i n
,wehave
i
2Th
(
[f%
1
;:::;%
i−
1
g
),
%
i
62 Th
(
[f%
1
;:::;%
i−
1
g
) (because of minimality of
^
) and
"
i
2 [f%
1
;:::;%
i−
1
g
. Consequently,
F 2Th
(
Ψ
n
+1
)
S
i
=0
Ψ
i
.
b) Let
` 2
^
. An argument similar to the one in clause (a) ensures that
` 2
n
S
i
=0
i
for some
n 2
IN
0
.
2. To show
S
i
=0
i
, we prove by induction that
Ψ
n
Ψ
and
n
^
for all
n 2
IN
0
. The base case,
n
= 0, holds by
denition since
Ψ
0
=
Ψ Ψ
and
0
=
^
S
i
=0
Ψ
i
and
Ψ
^
. Suppose
n>
0 and
assume that the claim holds for
n −
1.
a) If
F 2Th
(
Ψ
n−
1
), then the induction hypothesis
Ψ
n−
1
Ψ
implies
F 2Th
(
Ψ
)=
Ψ
.
b) If
F
=
%
for some
"
causes
%
if
2R
such that
2 Ψ
n−
1
and
" 2
n−
1
, then the induction hypothesis
Ψ
n−
1
Ψ
and
n−
1
^
,
respectively, implies
2 Ψ
and
" 2
^
. Consequently,
% 2 Ψ
and
^
% 2
.
Qed.
We are now prepared for a formal proof of the announced subsumption
result. That is, we will show that the successive application of causal relation-
ships to preliminary successors enables us to encounter all causal minimizing-
change successors.
Theorem 2.6.1.
Let
(
E; F; A; L
)
be a basic action domain and C and R
be sets of state constraints and causal relationships, respectively. Furthermore,
let S be an acceptable state and a an action. Then each causal minimizing-
change successor of S and a is also causal successor state.
Proof.
Let
T
be a causal minimizing-change successor obtained through ac-
tion law
a
transforms
C
into
E 2L
. Let
Ψ
=(
S \ T
)
[ E
and
=
E
,
then
T
=
f`
:((
S \ T
)
[ E;E
)
R
`g
implies
Th
(
T
)=
Ψ
=
S
i
=0
Ψ
i
where
(
Ψ;
^
)=
Th
R
(
Ψ;
).
We prove by induction that, for each
n 2
IN
0
,((
SnC
)
[E;E
)
;
R
(
S
n
;E
n
)
for some (
S
n
;E
n
) such that
Ψ
n
Th
(
S
n
) and
n
=
E
n
. Notice that each
Ψ
n
(
n
0) is consistent as
Ψ
n
Th
(
T
) and
T
is a state.
In case
n
= 0, let
S
0
=(
S n C
)
[ E
and
E
0
=
E
, which together satisfy
the claim: Consistency of
Ψ
0
=(
S \ T
)
[ E
and (
S n C
)
[ E
being a state
implies (
S \ T
)
[ E
(
S n C
)
[ E
, hence
Ψ
0
S
0
. Set
E
0
equals
0
by
denition.
For the induction step, let
n>
0 and suppose that some (
S
n−
1
;E
n−
1
)
satises the claim. Let
