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.
Search WWH ::




Custom Search