Information Technology Reference
In-Depth Information
2
4
3
5
(3.8)
Result
(
a
;s
)
^
Holds
(
:disq
(
a
)
;s
)
^
Successor
(
s; a; s
0
)
Qualied
([
a
ja
])
Qualied
(
a
)
^9s; s
0
The second axiom denes, in words, an action sequence [
a
ja
] to be qualied
if so is
a
, if the result
s
of performing
a
does not entail an abnormal dis-
qualication as regards
a
, and if there exists a successor
s
0
of
s
and
a
. The
reader may liken this to the notion of the model component
Res
being de-
ned for the argument [
a
ja
] (c.f. Denitions 3.3.1 and 3.3.2 in Section 3.3).
No further foundational axioms introduced in Chapter 2 require replacement.
Example 3.6.1.
Let
D
be the qualication domain consisting of the en-
tity
runs
0
,
in
1
,
mysterious
(
ignite
)
0
,
disq
(
ignite
)
0
,
pt
; fluent names
so that only
is an abnormality fluent; the partial priority ordering
runs
given by
ignite
0
; action law
ignite
transforms
f:
runs
g
into
f
runs
g
; and the steady state constraint
(
)
<
(
); action name
in
pt
mysterious
ignite
disq
(
ignite
)
9x:
in
(
x
)
_
mysterious
(
ignite
)
Let
FC
D
denote the Fluent Calculus-based axiomatization of this domain
as described in Chapter 2 (c.f. Section 2.9.2). Consider, then, the collection
of classical formulas
FC
D
[f
(3.7),(3.8), (2.37){(2.40)
g
, and suppose that
:Qualied
([
ignite
]) is true. The latter, in conjunction with axioms (3.7)
and (3.8), implies that for all
s; s
0
we have
;s
0
) (3.9)
:Result
([ ]
;s
)
_:Holds
(
:disq
(
ignite
)
;s
)
_:Successor
(
s;
ignite
The domain-independent axioms entail
9s
[
Result
([ ]
;s
)
^ State
(
s
) ]. Correct-
ness of
FC
D
moreover ensures that
State
(
s
)
8s
0
: :Successor
(
s;
ignite
;s
0
)
is entailed i so is
Holds
(
runs
;s
), for
:
runs
is the one and only regular pre-
condition of action
. Put together, the disjunction (3.9) implies the
ignite
following.
8s
[
Result
([ ]
;s
)
Holds
(
disq
(
ignite
)
;s
)
_ Holds
(
runs
;s
)]
That is to say,
ignite
being unexecutable, i.e.,
:Qualied
([
ignite
]), im-
plies either an abnormal disqualication or that the engine is already running.
On the analogy of a result in Chapter 2, a one-to-one correspondence
holds between the classical models of
FC
D
[f
(3.7),(3.8),(2.37){(2.40)
g
and
the interpretations for qualication scenarios of domain
D
. More precisely,
let
be some model of the aforementioned collection of classical formulas
and
I
=(
;Res
) an interpretation for a scenario (
O; D
). Then we say that
and
I correspond
i for all action sequences
a
, states
S
, and collections
of fluent literals
s
such that
EUNA j
=
s
=
S
, we nd that
Res
(
a
)=
S
i [
Result
(
a
;s
)]
is true
On this basis we can prove the following:
