Information Technology Reference
In-Depth Information
Proposition 2.9.1.
Let A and B be two sets of fluent literals.
1. If A B, then EUNA j
=
9z:
A
z
=
B
, else EUNA j
=
8z:
A
z 6
=
B
.
2. If A B, then EUNA j
=
8z
[
A
z
=
B
z
=
BnA
]
.
3. If A \ B
=
fg, then EUNA j
=
8z
[
z
=
A
B
z
=
A[B
]
.
Proof.
1. Suppose
A B
and let
Z
=
B n A
. Then
A
Z
and
B
are AC1N-
equal. Since
EUNA
includes AC1N, it entails
A
Z
=
B
, hence also
9z:
A
z
=
B
. Suppose
A 6 B
, then
A
z
and
B
are not AC1N-
uniable. According to clause 3a in Annotation 2.1, this implies
EUNA
entails
8z:
A
z 6
=
B
.
2. Let
z
be an arbitrary term, then
A
z
and
B
are AC1N-equal i each
fluent literal occurring in
A
z
also occurs in
B
and vice versa and no
fluent literal occurs twice or more in
A
z
. This in turn is equivalent to
z
and
BnA
being AC1N-equal (given that
A B
), hence is equivalent
to
z
=
BnA
under
EUNA
.
3. An arbitrary term
z
and the term
A
B
are AC1N-equal i each fluent
literal occurring in
z
also occurs in
A
B
and vice versa and no fluent
literal occurs twice or more in
z
(given that
A \ B
=
fg
). This in turn
is equivalent to
z
and
A[B
being AC1N-equal, hence is equivalent to
z
=
A[B
under
EUNA
.
Qed.
For illustration, consider
A
=
f
up
(
s
2
)
g
,
B
=
f:
up
(
s
1
)
;
up
(
s
2
)
; :
light
g
,
and
C
=
f
up
(
s
1
)
;
light
g
. Then
A B
and
A \ C
=
fg
. Accordingly,
EUNA
entails each of the following.
9z:
up
(
s
2
)
z
=
:
up
(
s
1
)
up
(
s
2
)
:
light
8z
[
up
(
s
2
)
z
=
:
up
(
s
1
)
up
(
s
2
)
:
light
z
=
:
up
(
s
1
)
:
light
]
8z
[
z
=
up
(
s
2
)
up
(
s
1
)
light
z
=
up
(
s
1
)
up
(
s
2
)
light
]
Clause 2 of the proposition will be particularly useful when axiomatizing
the application of action laws: Suppose
C
be the condition of some action
law,
S
be some state, and
z
be a term such that
EUNA j
=
C
z
=
S
,
then we know that
z
represents the set
S n C
. Precisely this is the reason
why idempotency of function
is not stipulated. For if it would be, then
C
z
=
S
would not imply
z
=
SnC
. Rather for any set
A
we would have
A
A
=
A
. But clearly
A
6
=
AnA
unless
A
=
fg
. In contrast,
EUNA
as
it stands entails
A
A
6
=
A
except for
A
=
;
, i.e.,
A
=
fg
.
With the extended unique name assumption,
EUNA
, and its properties
we are prepared for dening the circumstances under which a term represents
a state. In what follows, we tacitly assume a xed set of entities and fluent
names. We use a many-sorted logic language with ve sorts, namely, entities,
fluent literals, collections of fluent literals, actions, and sequences of actions.
Collections are composed of fluent literals, constant
;
, and our connection
function
. Below, variables of sort entity are indicated by
x
, variables of sort
