Information Technology Reference
In-Depth Information
In order that this conclusion is granted, an additional so-called frame axiom
is required, namely,
x 6
=
y ^
up
(
y; s
)
up
(
y; Do
(
toggle
(
x
)
;s
))
Now, the Frame Problem concerns the need for a large number of these
frame axioms (the
representational
aspect of the problem) and the necessity
to carry, one-by-one, each unchanged property to the next situation (the
inferential
aspect).
It took more than two decades to solve the representational aspect to the
best possible extent. The approach [86] is based on pure classical logic and
completely avoids the specication of frame axioms. This is accomplished by
combining, separately for each fluent, in a single eect axiom all possibilities
of how the fluent may change to true and to false, respectively. By virtue of
being bi-conditionals, these so-called successor state axioms implicitly contain
sucient information to also entail any
non
-change of the fluent in question.
An example is
up
(
x; Do
(
a; s
))
a
=
toggle
(
x
)
^:
up
(
x; s
)
_:
[
up
(
x; s
)
a
=
toggle
(
x
)]
Given
:
(
s
1
;S
0
)
^
(
s
2
;S
0
), this axiom entails
(
s
1
; Do
(
(
s
1
)
;S
0
))
up
up
up
toggle
and also
s
1
)
6
=
toggle
(
s
2
). While the concept of successor state axioms perfectly solves the
representational aspect of the Frame Problem, it does not at all address the
inferential aspect. For it still requires, for each non-aected fluent, separate
application of one of these axioms in order to conclude that the fluent keeps
its truth-value in the resulting situation.
The S
trips
framework [27] was an early development in response to the
inferential challenge raised by the Frame Problem. S
trips
encodes states
as sets of fluents, and the performance of actions is specied operationally,
namely, by removal and addition of certain fluents to these sets. Apparently,
this avoids investigation of any non-aected fluent. In compensation, the
operational, non-declarative nature of this approach causes the loss of both
expressiveness and flexibility of logic. With the aim of regaining the latter
without losing the computational merits of S
trips
, the
Linear Connection
Method
has been developed in [9], a precursor of
Linear Logic
[39]. It employs
a non-classical, resource-sensitive implication that allows to specify eects of
actions as straightforward as in
(
s
2
; Do
(
(
s
1
)
;S
0
)), tacitly assuming that
(
up
toggle
toggle
:
up
(
x
)&
Sit
(
s
) (
up
(
x
)&
Sit
(
Do
(
toggle
(
x
)
;s
))
(2.53)
where \ & " denotes a non-idempotent conjunction, \ ( " the aforemen-
tioned, non-classical implication, and
Sit
(
s
) should be read as \the cur-
rent situation is
s
." Being resource-sensitive, the antecedent of an impli-
cation like (2.53) is `consumed' whenever deriving the consequent. Conse-
quently,
:
up
(
s
1
)&
up
(
s
2
)&
Sit
(
S
0
), say, in conjunction with formula (2.53)
