Information Technology Reference
In-Depth Information
therefore we expect the circumscription of (Y
1
) to (Y
7
) to have the following
consequence:
¬Holds(Alive, Result(Shoot,Result(Wait,Result(Load,S
0
))))
(2.39)
However, (2.37) does not follow from the circumscription.
Proposition 2.1
(The Hanks-McDermott problem) If
Σ
is the conjunction of (Y
1
)
to (Y
7
) then,
CIRC[Σ∧(F2); Ab ; Holds] |≠
¬Holds(Alive, Result(Shoot, Result(Wait, Result(Load, S
0
))))
This proposition can be proved as follows:
Consider any model M of Σ∧(F
2
) that meets the following criteria:
M |= Holds( Loaded, Result(Load, S
0
))
M |= ¬Holds(Loaded, Result(Wait, Result(Load, S
0
))))
M |= Holds(Alive, Result(Shoot, Result(Wait, Result(Load, S
0
))))
It is easy to see that such models exist, and they will have the following
properties:
M |= Ab( Load, Loaded, S
0
)
M |= Ab(Wait, Loaded, Result(Load, S
0
))
M |= ¬Ab(Shoot, Alive, Result(Wait, Result(Load, S
0
)))
Then, with respect to the predicate Ab and Holds, it is obvious that we cannot
remove either of the above properties and still have a model. Therefore, some of
those models are minimal. Furthermore, since in any of these models we have
M |= Holds(Alive, Result(Shoot, Result(Wait, Result(Load, S
0
))))
We also have
CIRC[Σ∧(F
2
); Ab ; Holds] |≠ ¬Holds(Alive, Result(Shoot, Result(Wait,
Result(Load, S
0
))))
The Hanks and McFermott problem arises from a failure to respect the
directionality of time. This failure is most dramatically highlighted when default
logic is used to address the frame problem.
