Information Technology Reference
In-Depth Information
entails
(
s
1
)&
(
s
2
)&
Sit
(
Do
(
(
s
1
)
;S
0
)) but not the contradiction
up
up
toggle
:
s
1
)
;S
0
)). A compari-
son between Linear Connection Method and Situation Calculus can be found
in [8]. A thorough study of the relationship with Linear Logic is reported
in [29], where also an inference engine for the Linear Connection Method is
described.
The Fluent Calculus paradigm [51], so named by [12], embeds in pure clas-
sical logic the notion of resource-sensitivity as means to reflect the dynamics
of state transitions. For a specic class of planning problems, axiomatizations
based on Linear Connection Method, Fluent Calculus, and Linear Logic (in
the variant of [72]) have been proved equivalent [45]. In [118] it is shown
that under the provision that actions do not have an unbounded number of
direct eects, any Situation Calculus specication along the line of [86] can
be transformed into an essentially equivalent Fluent Calculus specication,
in which at the same time the representational and the inferential aspect of
the Frame Problem are addressed. Axiomatizations using the paradigm of
Fluent Calculus have been developed for a variety of ontological aspects|we
just mention concurrency of actions [12], continuous change [50, 117], hier-
archical planning [25], and nondeterministic [119] and complex actions [52].
Fluent Calculus grounds on the algebraic theory of Abelian monoid, which
is given by the axioms of associativity, commutativity, and existence of a
unit element. Unication algorithms specialized in this equational theory are
described in, e.g., [105, 16, 44] (for an overview see [80]). An analysis of com-
plexity is performed in [56]. The related notion of unication completeness
has been developed in the context of logic programming. Introductions to this
principle can be found in, e.g., [54, 101, 111]. The existence of a unication
complete theory for AC1 has been shown in [53].
(
s
1
)&
(
s
2
)&
Sit
(
S
0
)&
(
s
1
)&
Sit
(
Do
(
(
up
up
up
toggle
