Information Technology Reference
In-Depth Information
fluent literal by
`
, variables of sort action name by
a
, and variables of sort
action sequence by
a
, sometimes with sub- or superscripts. All other vari-
ables are of sort collection. Free variables are implicitly assumed universally
quantied.
To begin, the following axiom denes a predicate
Holds
(
`; s
) with the
intended meaning that
`
is contained in
s
:
Holds
(
`; s
)
9z: ` z
=
s
(2.20)
Let, for instance,
s
=
:
up
(
s
1
)
up
(
s
2
)
light
, then
Holds
(
up
(
s
2
)
;s
) and
:Holds
(
up
(
s
1
)
;s
) . The next axiom determines the constitutional properties
of state terms.
State
(
s
)
8`
[
Holds
(
`; s
)
:Holds
(
:`; s
)]
^8`; z: s 6
=
` ` z
(2.21)
In words,
s
represents a state if it contains each fluent literal or its negation
but not both. Furthermore, no fluent literal may occur twice (or more) in
s
.
For example, term
s
above satises
State
(
s
) provided our action domain is
based on exactly the three fluents of which
s
is composed. If so, then we also
have
:State
(
:
up
(
s
1
)
light
),
:State
(
:
up
(
s
1
)
up
(
s
1
)
up
(
s
2
)
light
),
and
:State
(
:
up
(
s
1
)
:
up
(
s
1
)
up
(
s
2
)
light
). The following proposition
justies our denition of
State
:
Proposition 2.9.2.
For a collection s, EUNA;
(2
:
20)
;
(2
:
21)
j
=
State
(
s
)
i
EUNA j
=
s
=
S
for some state S, else EUNA;
(2
:
20)
;
(2
:
21)
j
=
:State
(
s
)
.
Proof.
We have
EUNA;
(2
:
20)
;
(2
:
21)
j
=
State
(
s
)i
EUNA
and the ax-
ioms (2.20) and (2.21) entail
(
9z: ` z
=
s 8z
0
: :` z
0
6
=
s
)
^8z: s 6
=
` ` z
(2.22)
for each fluent literal
`
.
\
)
":
Suppose
EUNA
entails formula (2.22) for each fluent literal
`
. Dene
S
=
f`
:
EUNA j
=
9z: ` z
=
sg
, then entailment of the rst conjunct
of (2.22) ensures that
S
is a state. It also ensures that
S
consists of pre-
cisely the fluent literals which occur in
s
. Entailment of the second conjunct
of (2.22) moreover guarantees that no fluent literal occurs twice or more in
s
.
Altogether this implies
EUNA j
=
s
=
S
.
\
(
":
Suppose
EUNA j
=
s
=
S
for some state
S
. Then all fluent literals in
S
occur exactly once in
s
. Let
`
be a fluent literal.
S
being a state implies
that
f`gS
i
f:`g6S
. Thus, clause 1 of Proposition 2.9.1 ensures that
the rst conjunct of (2.22) is entailed. Moreover, since
s
does not contain
any literal twice or more,
s
and
` ` z
are not AC1N-uniable. This
implies
EUNA j
=
8z: s 6
=
` ` z
according to clause 3a in Annotation 2.1.
Altogether, it follows that
EUNA
entails formula (2.22) for each literal
`
.
Qed.