Information Technology Reference
In-Depth Information
1.
C S
(according to clause 1 of Proposition 2.9.1), and
2.
EUNA j
=
s
0
=
(
SnC
)
[E
(according to clauses 2 and 3 of Proposi-
tion 2.9.1 given that (
S n C
)
\ E
=
fg
, which is due to
kCk
=
kEk
).
These conditions are equivalent to action law
a
transforms
C
into
E
being
applicable to
S
and resulting in
S
0
=(
S n C
)
[ E
where
EUNA j
=
s
0
=
S
0
;
hence, the conditions are equivalent to
S
0
being a preliminary successor of
S
and
a
.
Qed.
As an example, consider the state
f:
(
s
1
)
;
(
s
2
)
; :
g
and the action
up
up
light
law instance
(
s
1
) transforms
f:
(
s
1
)
g
into
f
(
s
1
)
g
. Then
EUNA
toggle
up
up
entails
^ s
0
=
z
s
1
)]
with
s
0
=
up
(
s
1
)
up
(
s
2
)
:
light
, because
z
can be substituted by the
term
up
(
s
2
)
:
light
. Notice that
s
0
9z
[
:
up
(
s
1
)
z
=
:
up
(
s
1
)
up
(
s
2
)
:
light
up
(
represents the expected preliminary
successor state.
Subsequent to the generation of some preliminary successor is the (pos-
sibly repeated) application of causal relationships. Let the underlying set of
steady relationships be
f r
1
[
x
1
]=
"
1
causes
%
1
if
1
;:::;r
m
[
x
m
]=
"
m
causes
%
m
if
m
g
These relationships dene the ternary predicate
Causal
s
(
`
"
;`
%
;s
), an in-
stance of which is true if and only if there exists a steady causal relationship
with triggering eect
`
"
and ramication
`
%
and whose context holds in
state
s
, that is,
_
Causal
s
(
`
"
;`
%
;s
)
9x
i
[
`
"
=
"
i
^ `
%
=
%
i
^ Holds
(
i
;s
) ]
(2.26)
i
=1
Likewise, let
fr
1
[
x
1
]=
"
1
causes
%
1
if
1
;:::;r
n
[
x
n
]=
"
n
causes
%
n
if
n
g
be the underlying entire set of causal relationships, which dene predi-
cate
Causal
as follows:
_
Causal
(
`
"
;`
%
;s
)
9x
i
[
`
"
=
"
i
^ `
%
=
%
i
^ Holds
(
i
;s
) ]
(2.27)
i
=1
E.g., recall the following familiar four (non-steady) causal relationships.
up
(
s
1
) causes
light
if
up
(
s
2
)
:
up
(
s
1
) causes
:
light
if
>
up
(
s
2
) causes
light
if
up
(
s
1
)
:
up
(
s
2
) causes
:
light
if
>
These are encoded as
Causal
(
`
"
;`
%
;s
)
`
"
=
up
(
s
1
)
^ `
%
=
light
^ Holds
(
up
(
s
2
)
;s
)
_ `
"
=
up
(
s
2
)
^ `
%
=
light
^ Holds
(
up
(
s
1
)
;s
)
_ `
"
=
:
up
(
s
1
)
^ `
%
=
:
light
_ `
"
=
:
up
(
s
2
)
^ `
%
=
:
light
(2.28)
