Information Technology Reference
In-Depth Information
where the special constant
;
denotes a unit element for function
. This
constant will prove useful as formal counterpart of the empty collection of
fluent literals. The four axioms (AC1N, for short) constitute an equational
theory. Given the law of associativity, from now on we omit parentheses on
the level of
. Notice that the axioms AC1N formalize essential properties
of the mathematical concept of a set: The order in which set elements are
enumerated is irrelevant, too. From this perspective, constant
;
closely cor-
responds to the empty set.
19
For formal reasons, we introduce a function
which maps nite sets of fluent expressions
A
=
f`
1
;:::;`
n
g
to their term
representation
A
=
`
1
`
n
(including
fg
=
;
).
In conjunction with the standard axioms of equality, equational the-
ory AC1N entails the equivalence of two state terms whenever they are built
up from an identical collection of fluent literals. By standard equality axioms
we mean the following collection:
x
=
x
x
=
y y
=
x
x
=
y ^ y
=
z x
=
z
x
i
=
y f
(
x
1
;:::;x
i
;:::;x
n
)=
f
(
x
1
;:::;y;:::;x
n
)
x
i
=
y
[
P
(
x
1
;:::;x
i
;:::;x
n
)
P
(
x
1
;:::;y;:::;x
n
)]
(2.18)
for each
n
-place function symbol
f
and predicate
P
(
n
1), and for each
1
i n
. All variables are universally quantied.
AC1N plus these standard axioms alone, however, will not suce for an
axiomatization of our action theory. For it will also be necessary to prove
unequal two state terms which do not contain the same fluent literals. That
is, denials of equalities such as
s
2
) need also be
derivable. Notice that this inequation is not entailed by the above axioms, for
this would require the basic inequality
s
1
6
=
s
2
, which is nowhere granted.
The standard so-called assumption of unique names provides us with these
basic inequalities by means of additional axioms stating that syntactically
dierent terms are never equal. The presence of an equational theory ne-
cessitates a weakened version of this assumption. For
up
(
s
1
)
light
and
light
up
(
s
1
), say,
are
syntactically dierent but considered equal by our
axioms AC1N. A general concept known as
unication completeness
serves
this purpose. For a formal introduction to unication complete theories see
Annotation 2.1. The set of axioms which constitute an AC1N-unication
complete theory allows to derive inequality of state terms not representing
the identical collection of fluent literals. These axioms, which include AC1N
and the standard axioms of equality, shall be called
extended unique name
assumption
, abbreviated
EUNA
.
up
(
s
1
)
light
6
=
light
up
(
19
The reader may wonder why we do not additionally require function
to
be idempotent, i.e.,
8x: x x
=
x
, which the comparison with sets would
naturally suggest. The (subtle) reason for this decision is given below, right
after Proposition 2.9.1.
