Information Technology Reference
In-Depth Information
Application of (steady) causal relationships to state-eect pairs is axiom-
atized by dening the predicates
Causes
s
(
s; e; s
0
;e
0
) and
Causes
(
s; e; s
0
;e
0
),
respectively, an instance of which is true i some (steady) causal relationship
is applicable to (
s; e
) and yields (
s
0
;e
0
):
Causes
s
(
s; e; s
0
;e
0
)
8
<
9
=
Causal
s
(
`
"
;`
%
;s
)
^9v: "
i
v
=
e
^
9z
[
:%
i
z
=
s ^ s
0
=
z %
i
]
^
(2.29)
9`
"
;`
%
2
3
:
;
8w: :%
i
w 6
=
e ^ e
0
=
e %
i
_
9w
[
:%
i
w
=
e ^ e
0
=
w %
i
]
4
5
This denition needs explanation. Let
"
causes
%
if
be some steady causal
relationship whose context,
, holds in state
s
. Furthermore, let
S; E; S
0
;E
0
be the sets of fluent literals represented by
s; e; s
0
;e
0
. Then the equational
formula in the rst row on the right hand side of the equivalence encodes
condition
" 2 E
. The second row simultaneously models the two conditions
:% 2 S
and
S
0
=(
S nf:%g
)
[f%g
. Finally, axiomatizing the condition
that
E
0
=(
E nf:%g
)
[f%g
requires case analysis: If
:% 62 E
, then we
just have to add
%
to the corresponding term
e
(third row). If, on the
other hand,
:% 2 E
, then we have to additionally remove the sub-term
:%
from
e
(fourth row). The denition of
Causes
is analogous but with
Causal
replacing
Causal
s
.
Causes
(
s; e; s
0
;e
0
)
8
<
9
=
Causal
(
`
"
;`
%
;s
)
^9v: "
i
v
=
e
^
9z
[
:%
i
z
=
s ^ s
0
=
z %
i
]
^
(2.30)
9`
"
;`
%
2
3
:
;
8w: :%
i
w 6
=
e ^ e
0
=
e %
i
_
9w
[
:%
i
w
=
e ^ e
0
=
w %
i
]
4
5
Correctness of this axiomatization of causal relationships is given by the
following proposition.
Proposition 2.9.5.
Let R be a set of causal relationships. Furthermore, let
S be a state, E a set of fluent literals, and s
0
;e
0
two collections of fluent
literals. Then
EUNA;
(2
:
20)
;
(2
:
27)
;
(2
:
30)
j
=
Causes
(
S
;
E
;s
0
;e
0
)
(2.31)
i there exist two sets of fluent literals S
0
;E
0
such that
(
S; E
)
;
R
(
S
0
;E
0
)
and EUNA j
=
s
0
=
S
0
^ e
0
=
E
0
, else
EUNA;
(2
:
20)
;
(2
:
27)
;
(2
:
30)
j
=
:Causes
(
S
;
E
;s
0
;e
0
)