Information Technology Reference
In-Depth Information
Now, suppose
O
consists of the observations
:
runs
after []
inexecutable after []
ignite
We have already seen that
W
(
O;D
)
and the axiomatization of the second
observation, viz.
Qualied
([ ])
^:Qualied
([
]), entail
8s
[
Result
([ ]
;s
)
Holds
(
disq
(
ignite
)
;s
)
_ Holds
(
runs
;s
)]
The encoding of the rst observation, viz.
9s
[
Result
([ ]
;s
)
^Holds
(
:
runs
;s
)],
in conjunction with the axiom
Result
([ ]
;s
)
^ Result
([ ]
;s
0
)
s
=
s
0
ignite
allows
to strengthen the above to
8s
[
Result
([ ]
;s
)
Holds
(
disq
(
ignite
)
;s
)]
It follows that default
disq
(ignite)
cannot be applied. From the state con-
straint
disq
(
ignite
)
9x:
in
(
x
)
_
mysterious
(
ignite
)in
FC
D
we also
conclude that
8s
[
Result
([ ]
;s
)
9x: Holds
(
in
(
x
)
;s
)
_ Holds
(
mysterious
(
ignite
)
;s
)]
Since entity
is the only one, it follows that
in(pot)
and
mysterious(ignite)
are mutually exclusive, for either consequence in conjunction with
W
(
O;D
)
implies the negation of the other rule's justication. According to the prior-
ity ordering
<
D
, default
in(pot)
is to be preferably applied when seeking
prioritized extensions of
(
O;D
)
. Our default theory
(
O;D
)
thus admits a
unique prioritized extension
E
, which includes the following formula.
8s
[
Result
([ ]
;s
)
s
=
:
pt
(
)
:
(
)
disq
(
)]
runs
in
pt
mysterious
ignite
ignite
This formula is skeptically entailed by
(
O;D
)
. The reader may notice that ac-
cordingly the qualication scenario (
O; D
) admits a unique preferred model
(
;Res
), which satises
Res
([ ]) =
f:
runs
;
in
(
pt
)
; :
mysterious
(
ignite
)
; disq
(
ignite
)
g
In the remainder of this section, we prove general correctness of our ax-
iomatization of qualication scenarios by means of Prioritized Default Logic.
Some preparations are required to this end. Let
(
O;D
)
be the axiomati-
zation of a qualication scenario (
O; D
) with
F
ab
being the abnormality
fluents. Then a prioritized extension
E
of
(
O;D
)
and an interpretation
(
;Res
) for this scenario are said to
correspond
i for all
f
ab
2F
ab
we nd
that
:f
ab
2 Res
([ ]) i
8s
[
Result
([ ]
;s
)
:Holds
(
f
ab
;s
)]
2 E
(3.14)
The notion of
potential extensions
to be introduced next will be crucial
for the proof of our main theorem. In what follows, for notational convenience
we use the abbreviation
Initially
(
:`
) for
8s
[
Result
([ ]
;s
)
:Holds
(
`; s
)].
Suppose
F
is a set of formulas which consists in the following:
